src/HOL/Metis_Examples/Abstraction.thy
author hoelzl
Tue Mar 23 16:17:41 2010 +0100 (2010-03-23)
changeset 35928 d31f55f97663
parent 33027 9cf389429f6d
child 36566 f91342f218a9
permissions -rw-r--r--
Generate image for HOL-Probability
     1 (*  Title:      HOL/Metis_Examples/Abstraction.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 
     4 Testing the metis method.
     5 *)
     6 
     7 theory Abstraction
     8 imports Main FuncSet
     9 begin
    10 
    11 (*For Christoph Benzmueller*)
    12 lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
    13   by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
    14 
    15 (*this is a theorem, but we can't prove it unless ext is applied explicitly
    16 lemma "(op=) = (%x y. y=x)"
    17 *)
    18 
    19 consts
    20   monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
    21   pset  :: "'a set => 'a set"
    22   order :: "'a set => ('a * 'a) set"
    23 
    24 declare [[ atp_problem_prefix = "Abstraction__Collect_triv" ]]
    25 lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
    26 proof (neg_clausify)
    27 assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"
    28 assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
    29 have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
    30   by (metis CollectD 0)
    31 show "False"
    32   by (metis 2 1)
    33 qed
    34 
    35 lemma Collect_triv: "a \<in> {x. P x} ==> P a"
    36 by (metis mem_Collect_eq)
    37 
    38 
    39 declare [[ atp_problem_prefix = "Abstraction__Collect_mp" ]]
    40 lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
    41   by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq);
    42   --{*34 secs*}
    43 
    44 declare [[ atp_problem_prefix = "Abstraction__Sigma_triv" ]]
    45 lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
    46 proof (neg_clausify)
    47 assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type) \<in> Sigma (A\<Colon>'a\<Colon>type set) (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set)"
    48 assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> (b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) a"
    49 have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
    50   by (metis SigmaD1 0)
    51 have 3: "(b\<Colon>'b\<Colon>type) \<in> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
    52   by (metis SigmaD2 0)
    53 have 4: "(b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
    54   by (metis 1 2)
    55 show "False"
    56   by (metis 3 4)
    57 qed
    58 
    59 lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
    60 by (metis SigmaD1 SigmaD2)
    61 
    62 declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect" ]]
    63 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
    64 (*???metis says this is satisfiable!
    65 by (metis CollectD SigmaD1 SigmaD2)
    66 *)
    67 by (meson CollectD SigmaD1 SigmaD2)
    68 
    69 
    70 (*single-step*)
    71 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
    72 by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 Un_empty_right vimage_Collect_eq vimage_def vimage_singleton_eq)
    73 
    74 
    75 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
    76 proof (neg_clausify)
    77 assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type)
    78 \<in> Sigma (A\<Colon>'a\<Colon>type set)
    79    (COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))"
    80 assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> a \<noteq> (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type)"
    81 have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
    82   by (metis 0 SigmaD1)
    83 have 3: "(b\<Colon>'b\<Colon>type)
    84 \<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)"
    85   by (metis 0 SigmaD2) 
    86 have 4: "(b\<Colon>'b\<Colon>type) \<in> Collect (COMBB (op = (a\<Colon>'a\<Colon>type)) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type))"
    87   by (metis 3)
    88 have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
    89   by (metis 1 2)
    90 have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
    91   by (metis 4 vimage_singleton_eq insert_def singleton_conv2 Un_empty_right vimage_Collect_eq vimage_def)
    92 show "False"
    93   by (metis 5 6)
    94 qed
    95 
    96 (*Alternative structured proof, untyped*)
    97 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
    98 proof (neg_clausify)
    99 assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))"
   100 have 1: "b \<in> Collect (COMBB (op = a) f)"
   101   by (metis 0 SigmaD2)
   102 have 2: "f b = a"
   103   by (metis 1 vimage_Collect_eq singleton_conv2 insert_def Un_empty_right vimage_singleton_eq vimage_def)
   104 assume 3: "a \<notin> A \<or> a \<noteq> f b"
   105 have 4: "a \<in> A"
   106   by (metis 0 SigmaD1)
   107 have 5: "f b \<noteq> a"
   108   by (metis 4 3)
   109 show "False"
   110   by (metis 5 2)
   111 qed
   112 
   113 
   114 declare [[ atp_problem_prefix = "Abstraction__CLF_eq_in_pp" ]]
   115 lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
   116 by (metis Collect_mem_eq SigmaD2)
   117 
   118 lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
   119 proof (neg_clausify)
   120 assume 0: "(cl, f) \<in> CLF"
   121 assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))"
   122 assume 2: "f \<notin> pset cl"
   123 have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF"
   124   by (metis SigmaD2 1)
   125 have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF"
   126   by (metis 3 Collect_mem_eq)
   127 have 5: "(cl, f) \<notin> CLF"
   128   by (metis 2 4)
   129 show "False"
   130   by (metis 5 0)
   131 qed
   132 
   133 declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]]
   134 lemma
   135     "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
   136     f \<in> pset cl \<rightarrow> pset cl"
   137 proof (neg_clausify)
   138 assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
   139 assume 1: "(cl, f)
   140 \<in> Sigma CL
   141    (COMBB Collect
   142      (COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))"
   143 show "False"
   144 (*  by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*)
   145   by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def)
   146 qed
   147 
   148 
   149 declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Int" ]]
   150 lemma
   151     "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   152    f \<in> pset cl \<inter> cl"
   153 proof (neg_clausify)
   154 assume 0: "(cl, f)
   155 \<in> Sigma CL
   156    (COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))"
   157 assume 1: "f \<notin> pset cl \<inter> cl"
   158 have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl" 
   159   by (insert 0, simp add: COMBB_def) 
   160 (*  by (metis SigmaD2 0)  ??doesn't terminate*)
   161 have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl"
   162   by (metis 2 Collect_mem_eq)
   163 have 4: "f \<notin> cl \<inter> pset cl"
   164   by (metis 1 Int_commute)
   165 have 5: "f \<in> cl \<inter> pset cl"
   166   by (metis 3 Int_commute)
   167 show "False"
   168   by (metis 5 4)
   169 qed
   170 
   171 
   172 declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Pi_mono" ]]
   173 lemma
   174     "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
   175    (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
   176 by auto
   177 
   178 declare [[ atp_problem_prefix = "Abstraction__CLF_subset_Collect_Int" ]]
   179 lemma "(cl,f) \<in> CLF ==> 
   180    CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   181    f \<in> pset cl \<inter> cl"
   182 by auto
   183 
   184 (*??no longer terminates, with combinators
   185 by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
   186   --{*@{text Int_def} is redundant*}
   187 *)
   188 
   189 declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]]
   190 lemma "(cl,f) \<in> CLF ==> 
   191    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
   192    f \<in> pset cl \<inter> cl"
   193 by auto
   194 (*??no longer terminates, with combinators
   195 by (metis Collect_mem_eq Int_commute SigmaD2)
   196 *)
   197 
   198 declare [[ atp_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]]
   199 lemma 
   200    "(cl,f) \<in> CLF ==> 
   201     CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
   202     f \<in> pset cl \<rightarrow> pset cl"
   203 by fast
   204 (*??no longer terminates, with combinators
   205 by (metis Collect_mem_eq SigmaD2 subsetD)
   206 *)
   207 
   208 declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]]
   209 lemma 
   210   "(cl,f) \<in> CLF ==> 
   211    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
   212    f \<in> pset cl \<rightarrow> pset cl"
   213 by auto
   214 (*??no longer terminates, with combinators
   215 by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
   216 *)
   217 
   218 declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]]
   219 lemma 
   220   "(cl,f) \<in> CLF ==> 
   221    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
   222    (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
   223 by auto
   224 
   225 declare [[ atp_problem_prefix = "Abstraction__map_eq_zipA" ]]
   226 lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
   227 apply (induct xs)
   228 (*sledgehammer*)  
   229 apply auto
   230 done
   231 
   232 declare [[ atp_problem_prefix = "Abstraction__map_eq_zipB" ]]
   233 lemma "map (%w. (w -> w, w \<times> w)) xs = 
   234        zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
   235 apply (induct xs)
   236 (*sledgehammer*)  
   237 apply auto
   238 done
   239 
   240 declare [[ atp_problem_prefix = "Abstraction__image_evenA" ]]
   241 lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)";
   242 (*sledgehammer*)  
   243 by auto
   244 
   245 declare [[ atp_problem_prefix = "Abstraction__image_evenB" ]]
   246 lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
   247        ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
   248 (*sledgehammer*)  
   249 by auto
   250 
   251 declare [[ atp_problem_prefix = "Abstraction__image_curry" ]]
   252 lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" 
   253 (*sledgehammer*)  
   254 by auto
   255 
   256 declare [[ atp_problem_prefix = "Abstraction__image_TimesA" ]]
   257 lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
   258 (*sledgehammer*) 
   259 apply (rule equalityI)
   260 (***Even the two inclusions are far too difficult
   261 using [[ atp_problem_prefix = "Abstraction__image_TimesA_simpler"]]
   262 ***)
   263 apply (rule subsetI)
   264 apply (erule imageE)
   265 (*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)
   266 apply (erule ssubst)
   267 apply (erule SigmaE)
   268 (*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
   269 apply (erule ssubst)
   270 apply (subst split_conv)
   271 apply (rule SigmaI) 
   272 apply (erule imageI) +
   273 txt{*subgoal 2*}
   274 apply (clarify );
   275 apply (simp add: );  
   276 apply (rule rev_image_eqI)  
   277 apply (blast intro: elim:); 
   278 apply (simp add: );
   279 done
   280 
   281 (*Given the difficulty of the previous problem, these two are probably
   282 impossible*)
   283 
   284 declare [[ atp_problem_prefix = "Abstraction__image_TimesB" ]]
   285 lemma image_TimesB:
   286     "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" 
   287 (*sledgehammer*) 
   288 by force
   289 
   290 declare [[ atp_problem_prefix = "Abstraction__image_TimesC" ]]
   291 lemma image_TimesC:
   292     "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 
   293      ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 
   294 (*sledgehammer*) 
   295 by auto
   296 
   297 end