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