src/HOL/Metis_Examples/Abstraction.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 41144 509e51b7509a
child 42103 6066a35f6678
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (*  Title:      HOL/Metis_Examples/Abstraction.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Testing Metis.
     6 *)
     7 
     8 theory Abstraction
     9 imports Main "~~/src/HOL/Library/FuncSet"
    10 begin
    11 
    12 (*For Christoph Benzmueller*)
    13 lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
    14   by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
    15 
    16 (*this is a theorem, but we can't prove it unless ext is applied explicitly
    17 lemma "(op=) = (%x y. y=x)"
    18 *)
    19 
    20 consts
    21   monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
    22   pset  :: "'a set => 'a set"
    23   order :: "'a set => ('a * 'a) set"
    24 
    25 declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_triv" ]]
    26 lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
    27 proof -
    28   assume "a \<in> {x. P x}"
    29   hence "a \<in> P" by (metis Collect_def)
    30   hence "P a" by (metis mem_def)
    31   thus "P a" by metis
    32 qed
    33 
    34 lemma Collect_triv: "a \<in> {x. P x} ==> P a"
    35 by (metis mem_Collect_eq)
    36 
    37 
    38 declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_mp" ]]
    39 lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
    40   by (metis Collect_imp_eq ComplD UnE)
    41 
    42 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_triv" ]]
    43 lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
    44 proof -
    45   assume A1: "(a, b) \<in> Sigma A B"
    46   hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
    47   have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
    48   have "b \<in> B a" by (metis F1)
    49   thus "a \<in> A \<and> b \<in> B a" by (metis F2)
    50 qed
    51 
    52 lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
    53 by (metis SigmaD1 SigmaD2)
    54 
    55 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect" ]]
    56 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
    57 (* Metis says this is satisfiable!
    58 by (metis CollectD SigmaD1 SigmaD2)
    59 *)
    60 by (meson CollectD SigmaD1 SigmaD2)
    61 
    62 
    63 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
    64 by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq)
    65 
    66 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
    67 proof -
    68   assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
    69   have F1: "\<forall>u. {u} = op = u" by (metis singleton_conv2 Collect_def)
    70   have F2: "\<forall>y w v. v \<in> w -` op = y \<longrightarrow> w v = y"
    71     by (metis F1 vimage_singleton_eq)
    72   have F3: "\<forall>x w. (\<lambda>R. w (x R)) = x -` w"
    73     by (metis vimage_Collect_eq Collect_def)
    74   show "a \<in> A \<and> a = f b" by (metis A1 F2 F3 mem_Sigma_iff Collect_def)
    75 qed
    76 
    77 (* Alternative structured proof *)
    78 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
    79 proof -
    80   assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
    81   hence F1: "a \<in> A" by (metis mem_Sigma_iff)
    82   have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
    83   hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def)
    84   hence "a = f b" by (unfold mem_def)
    85   thus "a \<in> A \<and> a = f b" by (metis F1)
    86 qed
    87 
    88 
    89 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_in_pp" ]]
    90 lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
    91 by (metis Collect_mem_eq SigmaD2)
    92 
    93 lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
    94 proof -
    95   assume A1: "(cl, f) \<in> CLF"
    96   assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
    97   have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
    98   have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
    99   hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def)
   100   hence "f \<in> pset cl" by (metis A1)
   101   thus "f \<in> pset cl" by metis
   102 qed
   103 
   104 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]]
   105 lemma
   106     "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
   107     f \<in> pset cl \<rightarrow> pset cl"
   108 proof -
   109   assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
   110   have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
   111   have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
   112   hence "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
   113   thus "f \<in> pset cl \<rightarrow> pset cl" by metis
   114 qed
   115 
   116 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Int" ]]
   117 lemma
   118     "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   119    f \<in> pset cl \<inter> cl"
   120 proof -
   121   assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
   122   have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
   123   have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
   124   hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def)
   125   hence "f \<in> Id_on cl `` pset cl" by metis
   126   hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
   127   thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
   128 qed
   129 
   130 
   131 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi_mono" ]]
   132 lemma
   133     "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
   134    (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
   135 by auto
   136 
   137 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Int" ]]
   138 lemma "(cl,f) \<in> CLF ==> 
   139    CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   140    f \<in> pset cl \<inter> cl"
   141 by auto
   142 
   143 
   144 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]]
   145 lemma "(cl,f) \<in> CLF ==> 
   146    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   147    f \<in> pset cl \<inter> cl"
   148 by auto
   149 
   150 
   151 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]]
   152 lemma 
   153    "(cl,f) \<in> CLF ==> 
   154     CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
   155     f \<in> pset cl \<rightarrow> pset cl"
   156 by fast
   157 
   158 
   159 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]]
   160 lemma 
   161   "(cl,f) \<in> CLF ==> 
   162    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
   163    f \<in> pset cl \<rightarrow> pset cl"
   164 by auto
   165 
   166 
   167 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]]
   168 lemma 
   169   "(cl,f) \<in> CLF ==> 
   170    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
   171    (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
   172 by auto
   173 
   174 declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipA" ]]
   175 lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
   176 apply (induct xs)
   177  apply (metis map_is_Nil_conv zip.simps(1))
   178 by auto
   179 
   180 declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipB" ]]
   181 lemma "map (%w. (w -> w, w \<times> w)) xs = 
   182        zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
   183 apply (induct xs)
   184  apply (metis Nil_is_map_conv zip_Nil)
   185 by auto
   186 
   187 declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenA" ]]
   188 lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)"
   189 by (metis Collect_def image_subset_iff mem_def)
   190 
   191 declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenB" ]]
   192 lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
   193        ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
   194 by (metis Collect_def imageI image_image image_subset_iff mem_def)
   195 
   196 declare [[ sledgehammer_problem_prefix = "Abstraction__image_curry" ]]
   197 lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" 
   198 (*sledgehammer*)
   199 by auto
   200 
   201 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesA" ]]
   202 lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
   203 (*sledgehammer*)
   204 apply (rule equalityI)
   205 (***Even the two inclusions are far too difficult
   206 using [[ sledgehammer_problem_prefix = "Abstraction__image_TimesA_simpler"]]
   207 ***)
   208 apply (rule subsetI)
   209 apply (erule imageE)
   210 (*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)
   211 apply (erule ssubst)
   212 apply (erule SigmaE)
   213 (*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
   214 apply (erule ssubst)
   215 apply (subst split_conv)
   216 apply (rule SigmaI) 
   217 apply (erule imageI) +
   218 txt{*subgoal 2*}
   219 apply (clarify );
   220 apply (simp add: );  
   221 apply (rule rev_image_eqI)  
   222 apply (blast intro: elim:); 
   223 apply (simp add: );
   224 done
   225 
   226 (*Given the difficulty of the previous problem, these two are probably
   227 impossible*)
   228 
   229 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesB" ]]
   230 lemma image_TimesB:
   231     "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
   232 (*sledgehammer*)
   233 by force
   234 
   235 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesC" ]]
   236 lemma image_TimesC:
   237     "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 
   238      ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 
   239 (*sledgehammer*)
   240 by auto
   241 
   242 end