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