src/HOL/Metis_Examples/set.thy
author haftmann
Tue, 13 Jul 2010 16:00:56 +0200
changeset 37804 0145e59c1f6c
parent 37325 c2a44bc874f9
child 41144 509e51b7509a
permissions -rw-r--r--
qualified names for (almost) all array operations
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 32864
diff changeset
     1
(*  Title:      HOL/Metis_Examples/set.thy
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     3
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 32864
diff changeset
     4
Testing the metis method.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     5
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 32864
diff changeset
     7
theory set
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 32864
diff changeset
     8
imports Main
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     9
begin
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    10
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    11
lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    12
               (S(x,y) | ~S(y,z) | Q(Z,Z))  &
24742
73b8b42a36b6 removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents: 23519
diff changeset
    13
               (Q(X,y) | ~Q(y,Z) | S(X,X))" 
23519
a4ffa756d8eb bug fixes to proof reconstruction
paulson
parents: 23449
diff changeset
    14
by metis
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    15
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    16
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    17
by metis
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    18
36925
ffad77bb3046 renamed Sledgehammer options
blanchet
parents: 36573
diff changeset
    19
sledgehammer_params [isar_proof, isar_shrink_factor = 1]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    20
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    21
(*multiple versions of this example*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    22
lemma (*equal_union: *)
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 36407
diff changeset
    23
   "(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))"
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    24
proof -
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    25
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    26
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    27
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    28
  { assume "\<not> Z \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    29
    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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    30
  moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    31
  { assume AA1: "Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    32
    { assume "\<not> Y \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    33
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    34
    moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    35
    { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    36
      { assume "\<not> Z \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    37
        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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    38
      moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    39
      { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    40
        hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    41
        hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    42
        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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    43
        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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    44
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    45
    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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    46
  moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    47
  { 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"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    48
    { assume "\<not> Y \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    49
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    50
    moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    51
    { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    52
      { assume "\<not> Z \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    53
        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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    54
      moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    55
      { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    56
        hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    57
        hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    58
        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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    59
        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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    60
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    61
    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 }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    62
  moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    63
  { assume "\<not> Y \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    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 F1) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    65
  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
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    66
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    67
36925
ffad77bb3046 renamed Sledgehammer options
blanchet
parents: 36573
diff changeset
    68
sledgehammer_params [isar_proof, isar_shrink_factor = 2]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    69
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    70
lemma (*equal_union: *)
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    71
   "(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))"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    72
proof -
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    73
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    74
  { 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"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    75
    { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    76
      { assume "\<not> Z \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    77
        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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    78
      moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    79
      { assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    80
        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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    81
        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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    82
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    83
    moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    84
    { assume "\<not> Y \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    85
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    86
    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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    87
  moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    88
  { assume "\<not> Z \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    89
    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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    90
  moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    91
  { assume "\<not> Y \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    92
    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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    93
  moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    94
  { assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    95
    { assume "\<not> Z \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    96
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    97
    moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    98
    { assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
    99
      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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   100
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   101
    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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   102
  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
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   103
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   104
36925
ffad77bb3046 renamed Sledgehammer options
blanchet
parents: 36573
diff changeset
   105
sledgehammer_params [isar_proof, isar_shrink_factor = 3]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   106
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   107
lemma (*equal_union: *)
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   108
   "(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))"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   109
proof -
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   110
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   111
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   112
  { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   113
    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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   114
  moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   115
  { 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"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   116
    { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   117
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   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 AA1 Un_commute Un_subset_iff Un_upper2) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   119
  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)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   120
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   121
36925
ffad77bb3046 renamed Sledgehammer options
blanchet
parents: 36573
diff changeset
   122
sledgehammer_params [isar_proof, isar_shrink_factor = 4]
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   123
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   124
lemma (*equal_union: *)
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   125
   "(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))"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   126
proof -
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   127
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   128
  { assume "\<not> Y \<subseteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   129
    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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   130
  moreover
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   131
  { assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   132
    { 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"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   133
      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) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   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 AA1 F1 Un_commute Un_subset_iff Un_upper2) }
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   135
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   136
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   137
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   138
sledgehammer_params [isar_proof, isar_shrink_factor = 1]
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   139
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   140
lemma (*equal_union: *)
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   141
   "(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))"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   142
by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   143
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   144
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))"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   145
by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   146
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   147
lemma fixedpoint: "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   148
by metis
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   149
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   150
lemma (* fixedpoint: *) "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   151
proof -
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   152
  assume "\<exists>!x\<Colon>'a. f (g x) = x"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   153
  thus "\<exists>!y\<Colon>'b. g (f y) = y" by metis
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   154
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   155
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   156
lemma (* singleton_example_2: *)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   157
     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   158
by (metis Set.subsetI Union_upper insertCI set_eq_subset)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   159
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   160
lemma (* singleton_example_2: *)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   161
     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
32685
29e4e567b5f4 tuned proofs
haftmann
parents: 32519
diff changeset
   162
by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   163
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   164
lemma singleton_example_2:
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   165
     "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   166
proof -
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   167
  assume "\<forall>x \<in> S. \<Union>S \<subseteq> x"
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   168
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   169
  hence "\<forall>x\<^isub>1. x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis Union_upper)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   170
  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)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   171
  hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. S \<subseteq> insert (\<Union>S) x\<^isub>1" by (metis insert_iff)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   172
  thus "\<exists>z. S \<subseteq> {z}" by metis
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   173
qed
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   174
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   175
text {*
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   176
  From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   177
  293-314.
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   178
*}
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   179
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   180
(* Notes: (1) The numbering doesn't completely agree with the paper.
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   181
   (2) We must rename set variables to avoid type clashes. *)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   182
lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   183
      "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   184
      "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   185
      "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>B. a \<notin> B \<and> b \<in> B \<and> c \<notin> B"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   186
      "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   187
      "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   188
      "\<exists>A. a \<notin> A"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 36407
diff changeset
   189
      "(\<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"
37325
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   190
       apply (metis all_not_in_conv)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   191
      apply (metis all_not_in_conv)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   192
     apply (metis mem_def)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   193
    apply (metis less_int_def singleton_iff)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   194
   apply (metis mem_def)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   195
  apply (metis mem_def)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   196
 apply (metis all_not_in_conv)
c2a44bc874f9 redid the Isar proofs using the latest Sledgehammer, eliminating the last occurrences of "neg_clausify" in proofs
blanchet
parents: 36925
diff changeset
   197
by (metis pair_in_Id_conv)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   198
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   199
end