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