src/HOL/Metis_Examples/Abstraction.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46364 abab10d1f4a3
child 55465 0d31c0546286
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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/Abstraction.thy
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42757
diff changeset
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
41144
509e51b7509a example tuning
blanchet
parents: 38991
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     4
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42757
diff changeset
     5
Example featuring Metis's support for lambda-abstractions.
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     6
*)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
     7
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42757
diff changeset
     8
header {* Example Featuring Metis's Support for Lambda-Abstractions *}
c71657bbdbc0 tuned Metis examples
blanchet
parents: 42757
diff changeset
     9
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 26819
diff changeset
    10
theory Abstraction
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    11
imports "~~/src/HOL/Library/FuncSet"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    12
begin
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    13
45562
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
    14
(* For Christoph Benzm├╝ller *)
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
    15
lemma "x < 1 \<and> ((op =) = (op =)) \<Longrightarrow> ((op =) = (op =)) \<and> x < (2::nat)"
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
    16
by (metis nat_1_add_1 trans_less_add2)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    17
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    18
lemma "(op = ) = (\<lambda>x y. y = x)"
45562
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
    19
by metis
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    20
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    21
consts
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    22
  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    23
  pset  :: "'a set => 'a set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    24
  order :: "'a set => ('a * 'a) set"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    25
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    26
lemma "a \<in> {x. P x} \<Longrightarrow> P a"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    27
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    28
  assume "a \<in> {x. P x}"
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    29
  thus "P a" by (metis mem_Collect_eq)
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    30
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    31
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    32
lemma Collect_triv: "a \<in> {x. P x} \<Longrightarrow> P a"
23756
14008ce7df96 Adapted to changes in Predicate theory.
berghofe
parents: 23519
diff changeset
    33
by (metis mem_Collect_eq)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    34
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    35
lemma "a \<in> {x. P x --> Q x} \<Longrightarrow> a \<in> {x. P x} \<Longrightarrow> a \<in> {x. Q x}"
45562
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
    36
by (metis Collect_imp_eq ComplD UnE)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    37
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    38
lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A \<and> b \<in> B a"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    39
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    40
  assume A1: "(a, b) \<in> Sigma A B"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    41
  hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    42
  have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    43
  have "b \<in> B a" by (metis F1)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    44
  thus "a \<in> A \<and> b \<in> B a" by (metis F2)
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    45
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    46
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    47
lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    48
by (metis SigmaD1 SigmaD2)
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    49
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    50
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
46364
abab10d1f4a3 example tuning
blanchet
parents: 46076
diff changeset
    51
by (metis (full_types, lifting) CollectD SigmaD1 SigmaD2)
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    52
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    53
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    54
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    55
  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    56
  hence F1: "a \<in> A" by (metis mem_Sigma_iff)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    57
  have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    58
  hence "a = f b" by (metis (full_types) mem_Collect_eq)
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    59
  thus "a \<in> A \<and> a = f b" by (metis F1)
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    60
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    61
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    62
lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
    63
by (metis Collect_mem_eq SigmaD2)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    64
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    65
lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    66
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    67
  assume A1: "(cl, f) \<in> CLF"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    68
  assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    69
  have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    70
  hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis mem_Collect_eq)
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    71
  thus "f \<in> pset cl" by (metis A1)
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    72
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    73
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    74
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    75
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    76
   f \<in> pset cl \<rightarrow> pset cl"
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    77
by (metis (no_types) Collect_mem_eq Sigma_triv)
45562
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
    78
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    79
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    80
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    81
   f \<in> pset cl \<rightarrow> pset cl"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    82
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    83
  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    84
  have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    85
  thus "f \<in> pset cl \<rightarrow> pset cl" by (metis mem_Collect_eq)
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    86
qed
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    87
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
    88
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    89
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    90
   f \<in> pset cl \<inter> cl"
45562
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
    91
by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem)
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
    92
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    93
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    94
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
    95
   f \<in> pset cl \<inter> cl"
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    96
proof -
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    97
  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
    98
  have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
    99
  hence "f \<in> Id_on cl `` pset cl" by (metis Int_commute Image_Id_on mem_Collect_eq)
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   100
  hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   101
  thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   102
qed
24827
646bdc51eb7d combinator translation
paulson
parents: 24783
diff changeset
   103
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   104
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   105
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   106
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   107
by auto
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   108
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   109
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   110
  "(cl, f) \<in> CLF \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   111
   CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   112
   f \<in> pset cl \<inter> cl"
46364
abab10d1f4a3 example tuning
blanchet
parents: 46076
diff changeset
   113
by (metis (lifting) CollectD Sigma_triv subsetD)
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   114
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   115
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   116
  "(cl, f) \<in> CLF \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   117
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   118
   f \<in> pset cl \<inter> cl"
46364
abab10d1f4a3 example tuning
blanchet
parents: 46076
diff changeset
   119
by (metis (lifting) CollectD Sigma_triv)
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   120
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   121
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   122
  "(cl, f) \<in> CLF \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   123
   CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   124
   f \<in> pset cl \<rightarrow> pset cl"
46364
abab10d1f4a3 example tuning
blanchet
parents: 46076
diff changeset
   125
by (metis (lifting) CollectD Sigma_triv subsetD)
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   126
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   127
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   128
  "(cl, f) \<in> CLF \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   129
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   130
   f \<in> pset cl \<rightarrow> pset cl"
46364
abab10d1f4a3 example tuning
blanchet
parents: 46076
diff changeset
   131
by (metis (lifting) CollectD Sigma_triv)
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   132
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   133
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   134
  "(cl, f) \<in> CLF \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   135
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   136
   (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   137
by auto
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   138
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   139
lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   140
apply (induct xs)
45562
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
   141
 apply (metis map.simps(1) zip_Nil)
36566
f91342f218a9 redid some Sledgehammer/Metis proofs
blanchet
parents: 33027
diff changeset
   142
by auto
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   143
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   144
lemma
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   145
  "map (\<lambda>w. (w -> w, w \<times> w)) xs =
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   146
   zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   147
apply (induct xs)
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   148
 apply (metis map.simps(1) zip_Nil)
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   149
by auto
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   150
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   151
lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   152
by (metis mem_Collect_eq image_eqI subsetD)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   153
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   154
lemma
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   155
  "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   156
   (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   157
by (metis mem_Collect_eq imageI set_rev_mp)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   158
46076
a109eb27f54f ported a dozen of proofs to the "set" type constructor
blanchet
parents: 45972
diff changeset
   159
lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
46364
abab10d1f4a3 example tuning
blanchet
parents: 46076
diff changeset
   160
by (metis (lifting) imageE)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   161
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   162
lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
45562
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
   163
by (metis map_pair_def map_pair_surj_on)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   164
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   165
lemma image_TimesB:
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   166
    "(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)"
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   167
by force
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   168
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   169
lemma image_TimesC:
45572
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   170
  "(\<lambda>(x, y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
08970468f99b more "metis" calls in example
blanchet
parents: 45563
diff changeset
   171
   ((\<lambda>x. x \<rightarrow> x) ` A) \<times> ((\<lambda>y. y \<times> y) ` B)"
45562
e8fab4786b3c example cleanup
blanchet
parents: 45503
diff changeset
   172
by (metis image_TimesA)
23449
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   173
dd874e6a3282 integration of Metis prover
paulson
parents:
diff changeset
   174
end