src/HOL/Metis_Examples/Abstraction.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 55932 68c5104d2204
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
wenzelm@33027
     1
(*  Title:      HOL/Metis_Examples/Abstraction.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
Example featuring Metis's support for lambda-abstractions.
paulson@23449
     6
*)
paulson@23449
     7
blanchet@43197
     8
header {* Example Featuring Metis's Support for Lambda-Abstractions *}
blanchet@43197
     9
haftmann@27368
    10
theory Abstraction
blanchet@45572
    11
imports "~~/src/HOL/Library/FuncSet"
paulson@23449
    12
begin
paulson@23449
    13
blanchet@45562
    14
(* For Christoph Benzm├╝ller *)
blanchet@45562
    15
lemma "x < 1 \<and> ((op =) = (op =)) \<Longrightarrow> ((op =) = (op =)) \<and> x < (2::nat)"
blanchet@45562
    16
by (metis nat_1_add_1 trans_less_add2)
paulson@23449
    17
blanchet@45572
    18
lemma "(op = ) = (\<lambda>x y. y = x)"
blanchet@45562
    19
by metis
paulson@23449
    20
paulson@23449
    21
consts
paulson@23449
    22
  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
paulson@23449
    23
  pset  :: "'a set => 'a set"
paulson@23449
    24
  order :: "'a set => ('a * 'a) set"
paulson@23449
    25
blanchet@46076
    26
lemma "a \<in> {x. P x} \<Longrightarrow> P a"
blanchet@36566
    27
proof -
blanchet@36566
    28
  assume "a \<in> {x. P x}"
blanchet@46076
    29
  thus "P a" by (metis mem_Collect_eq)
blanchet@46076
    30
qed
paulson@23449
    31
blanchet@45572
    32
lemma Collect_triv: "a \<in> {x. P x} \<Longrightarrow> P a"
berghofe@23756
    33
by (metis mem_Collect_eq)
paulson@23449
    34
blanchet@45572
    35
lemma "a \<in> {x. P x --> Q x} \<Longrightarrow> a \<in> {x. P x} \<Longrightarrow> a \<in> {x. Q x}"
blanchet@45562
    36
by (metis Collect_imp_eq ComplD UnE)
paulson@23449
    37
blanchet@46076
    38
lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A \<and> b \<in> B a"
blanchet@36566
    39
proof -
blanchet@36566
    40
  assume A1: "(a, b) \<in> Sigma A B"
blanchet@36566
    41
  hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
blanchet@36566
    42
  have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
blanchet@36566
    43
  have "b \<in> B a" by (metis F1)
blanchet@36566
    44
  thus "a \<in> A \<and> b \<in> B a" by (metis F2)
blanchet@46076
    45
qed
paulson@23449
    46
blanchet@45572
    47
lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
paulson@23449
    48
by (metis SigmaD1 SigmaD2)
paulson@23449
    49
blanchet@36566
    50
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
blanchet@46364
    51
by (metis (full_types, lifting) CollectD SigmaD1 SigmaD2)
paulson@24827
    52
blanchet@46076
    53
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
blanchet@36566
    54
proof -
blanchet@36566
    55
  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
blanchet@36566
    56
  hence F1: "a \<in> A" by (metis mem_Sigma_iff)
blanchet@36566
    57
  have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
blanchet@46076
    58
  hence "a = f b" by (metis (full_types) mem_Collect_eq)
blanchet@36566
    59
  thus "a \<in> A \<and> a = f b" by (metis F1)
blanchet@46076
    60
qed
paulson@23449
    61
blanchet@45572
    62
lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
paulson@24827
    63
by (metis Collect_mem_eq SigmaD2)
paulson@23449
    64
blanchet@46076
    65
lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
blanchet@36566
    66
proof -
blanchet@36566
    67
  assume A1: "(cl, f) \<in> CLF"
blanchet@36566
    68
  assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
blanchet@36566
    69
  have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
blanchet@46076
    70
  hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis mem_Collect_eq)
blanchet@45572
    71
  thus "f \<in> pset cl" by (metis A1)
blanchet@46076
    72
qed
paulson@23449
    73
blanchet@46076
    74
lemma
blanchet@45572
    75
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
blanchet@45572
    76
   f \<in> pset cl \<rightarrow> pset cl"
blanchet@46076
    77
by (metis (no_types) Collect_mem_eq Sigma_triv)
blanchet@45562
    78
blanchet@46076
    79
lemma
blanchet@45572
    80
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
blanchet@45572
    81
   f \<in> pset cl \<rightarrow> pset cl"
blanchet@36566
    82
proof -
blanchet@36566
    83
  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
blanchet@36566
    84
  have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
blanchet@46076
    85
  thus "f \<in> pset cl \<rightarrow> pset cl" by (metis mem_Collect_eq)
blanchet@46076
    86
qed
paulson@23449
    87
paulson@23449
    88
lemma
blanchet@45572
    89
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
blanchet@45572
    90
   f \<in> pset cl \<inter> cl"
blanchet@45562
    91
by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem)
blanchet@45562
    92
blanchet@46076
    93
lemma
blanchet@45572
    94
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
blanchet@45572
    95
   f \<in> pset cl \<inter> cl"
blanchet@36566
    96
proof -
blanchet@36566
    97
  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
blanchet@36566
    98
  have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
blanchet@46076
    99
  hence "f \<in> Id_on cl `` pset cl" by (metis Int_commute Image_Id_on mem_Collect_eq)
blanchet@36566
   100
  hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
blanchet@36566
   101
  thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
blanchet@46076
   102
qed
paulson@24827
   103
paulson@23449
   104
lemma
blanchet@45572
   105
  "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
paulson@23449
   106
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
paulson@23449
   107
by auto
paulson@23449
   108
blanchet@46076
   109
lemma
blanchet@45572
   110
  "(cl, f) \<in> CLF \<Longrightarrow>
blanchet@45572
   111
   CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
blanchet@45572
   112
   f \<in> pset cl \<inter> cl"
blanchet@46364
   113
by (metis (lifting) CollectD Sigma_triv subsetD)
blanchet@36566
   114
blanchet@46076
   115
lemma
blanchet@45572
   116
  "(cl, f) \<in> CLF \<Longrightarrow>
blanchet@45572
   117
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
blanchet@45572
   118
   f \<in> pset cl \<inter> cl"
blanchet@46364
   119
by (metis (lifting) CollectD Sigma_triv)
blanchet@36566
   120
blanchet@46076
   121
lemma
blanchet@45572
   122
  "(cl, f) \<in> CLF \<Longrightarrow>
blanchet@45572
   123
   CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow>
blanchet@45572
   124
   f \<in> pset cl \<rightarrow> pset cl"
blanchet@46364
   125
by (metis (lifting) CollectD Sigma_triv subsetD)
blanchet@45572
   126
blanchet@46076
   127
lemma
blanchet@45572
   128
  "(cl, f) \<in> CLF \<Longrightarrow>
blanchet@45572
   129
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
blanchet@45572
   130
   f \<in> pset cl \<rightarrow> pset cl"
blanchet@46364
   131
by (metis (lifting) CollectD Sigma_triv)
blanchet@45572
   132
blanchet@46076
   133
lemma
blanchet@45572
   134
  "(cl, f) \<in> CLF \<Longrightarrow>
blanchet@45572
   135
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
blanchet@45572
   136
   (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
blanchet@46076
   137
by auto
paulson@23449
   138
blanchet@45572
   139
lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
paulson@23449
   140
apply (induct xs)
blanchet@55465
   141
 apply (metis list.map(1) zip_Nil)
blanchet@36566
   142
by auto
paulson@23449
   143
blanchet@45572
   144
lemma
blanchet@45572
   145
  "map (\<lambda>w. (w -> w, w \<times> w)) xs =
blanchet@45572
   146
   zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
blanchet@45572
   147
apply (induct xs)
blanchet@55465
   148
 apply (metis list.map(1) zip_Nil)
blanchet@45572
   149
by auto
blanchet@45572
   150
blanchet@46076
   151
lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
blanchet@46076
   152
by (metis mem_Collect_eq image_eqI subsetD)
paulson@23449
   153
blanchet@46076
   154
lemma
blanchet@45572
   155
  "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
blanchet@45572
   156
   (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
blanchet@46076
   157
by (metis mem_Collect_eq imageI set_rev_mp)
paulson@23449
   158
blanchet@46076
   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)"
blanchet@46364
   160
by (metis (lifting) imageE)
paulson@23449
   161
blanchet@45572
   162
lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
blanchet@55932
   163
by (metis map_prod_def map_prod_surj_on)
paulson@23449
   164
paulson@23449
   165
lemma image_TimesB:
blanchet@45572
   166
    "(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)"
paulson@23449
   167
by force
paulson@23449
   168
paulson@23449
   169
lemma image_TimesC:
blanchet@45572
   170
  "(\<lambda>(x, y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
blanchet@45572
   171
   ((\<lambda>x. x \<rightarrow> x) ` A) \<times> ((\<lambda>y. y \<times> y) ` B)"
blanchet@45562
   172
by (metis image_TimesA)
paulson@23449
   173
paulson@23449
   174
end