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