src/HOL/MetisExamples/Abstraction.thy
author berghofe
Wed Jul 11 11:29:44 2007 +0200 (2007-07-11)
changeset 23756 14008ce7df96
parent 23519 a4ffa756d8eb
child 24632 779fc4fcbf8b
permissions -rw-r--r--
Adapted to changes in Predicate theory.
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
paulson@23449
     8
theory Abstraction imports FuncSet
paulson@23449
     9
begin
paulson@23449
    10
paulson@23449
    11
(*For Christoph Benzmueller*)
paulson@23449
    12
lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
paulson@23449
    13
  by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
paulson@23449
    14
paulson@23449
    15
(*this is a theorem, but we can't prove it unless ext is applied explicitly
paulson@23449
    16
lemma "(op=) = (%x y. y=x)"
paulson@23449
    17
*)
paulson@23449
    18
paulson@23449
    19
consts
paulson@23449
    20
  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
paulson@23449
    21
  pset  :: "'a set => 'a set"
paulson@23449
    22
  order :: "'a set => ('a * 'a) set"
paulson@23449
    23
paulson@23449
    24
ML{*ResAtp.problem_name := "Abstraction__Collect_triv"*}
paulson@23449
    25
lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
paulson@23449
    26
proof (neg_clausify)
paulson@23449
    27
assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"
paulson@23449
    28
assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
paulson@23449
    29
have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
paulson@23449
    30
  by (metis CollectD 0)
paulson@23449
    31
show "False"
paulson@23449
    32
  by (metis 2 1)
paulson@23449
    33
qed
paulson@23449
    34
paulson@23449
    35
lemma Collect_triv: "a \<in> {x. P x} ==> P a"
berghofe@23756
    36
by (metis mem_Collect_eq)
paulson@23449
    37
paulson@23449
    38
paulson@23449
    39
ML{*ResAtp.problem_name := "Abstraction__Collect_mp"*}
paulson@23449
    40
lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
berghofe@23756
    41
  by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq);
paulson@23449
    42
  --{*34 secs*}
paulson@23449
    43
paulson@23449
    44
ML{*ResAtp.problem_name := "Abstraction__Sigma_triv"*}
paulson@23449
    45
lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
paulson@23449
    46
proof (neg_clausify)
paulson@23449
    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)"
paulson@23449
    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"
paulson@23449
    49
have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
paulson@23449
    50
  by (metis SigmaD1 0)
paulson@23449
    51
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
    52
  by (metis SigmaD2 0)
paulson@23449
    53
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
    54
  by (metis 1 2)
paulson@23449
    55
show "False"
paulson@23449
    56
  by (metis 3 4)
paulson@23449
    57
qed
paulson@23449
    58
paulson@23449
    59
lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
paulson@23449
    60
by (metis SigmaD1 SigmaD2)
paulson@23449
    61
paulson@23449
    62
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect"*}
paulson@23449
    63
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
paulson@23449
    64
(*???metis cannot prove this
paulson@23449
    65
by (metis CollectD SigmaD1 SigmaD2 UN_eq)
paulson@23449
    66
Also, UN_eq is unnecessary*)
paulson@23449
    67
by (meson CollectD SigmaD1 SigmaD2)
paulson@23449
    68
paulson@23449
    69
paulson@23449
    70
paulson@23449
    71
(*single-step*)
paulson@23449
    72
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
paulson@23449
    73
proof (neg_clausify)
paulson@23449
    74
assume 0: "(a, b) \<in> Sigma A (llabs_subgoal_1 f)"
paulson@23449
    75
assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"
paulson@23449
    76
assume 2: "a \<notin> A \<or> a \<noteq> f b"
paulson@23449
    77
have 3: "a \<in> A"
berghofe@23756
    78
  by (metis SigmaD1 0)
paulson@23519
    79
have 4: "f b \<noteq> a"
paulson@23519
    80
  by (metis 3 2)
paulson@23519
    81
have 5: "f b = a"
berghofe@23756
    82
  by (metis Domain_Id Compl_UNIV_eq singleton_conv2 vimage_Collect_eq 1 vimage_singleton_eq SigmaD2 0)
paulson@23449
    83
show "False"
paulson@23519
    84
  by (metis 5 4)
paulson@23449
    85
qed finish_clausify
paulson@23449
    86
paulson@23449
    87
paulson@23449
    88
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*}
paulson@23449
    89
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
paulson@23449
    90
apply (metis Collect_mem_eq SigmaD2);
paulson@23449
    91
done
paulson@23449
    92
paulson@23449
    93
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"proof (neg_clausify)
paulson@23449
    94
assume 0: "(cl, f) \<in> CLF"
paulson@23449
    95
assume 1: "CLF = Sigma CL llabs_subgoal_1"
paulson@23449
    96
assume 2: "\<And>cl. llabs_subgoal_1 cl =
berghofe@23756
    97
     Collect (llabs_List_Xlists_def_1_ (pset cl))"
paulson@23449
    98
assume 3: "f \<notin> pset cl"
paulson@23449
    99
show "False"
paulson@23449
   100
  by (metis 0 1 SigmaD2 3 2 Collect_mem_eq)
paulson@23449
   101
qed finish_clausify (*ugly hack: combinators??*)
paulson@23449
   102
paulson@23449
   103
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
paulson@23449
   104
lemma
paulson@23449
   105
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
paulson@23449
   106
    f \<in> pset cl \<rightarrow> pset cl"
paulson@23449
   107
apply (metis Collect_mem_eq SigmaD2);
paulson@23449
   108
done
paulson@23449
   109
paulson@23449
   110
lemma
paulson@23449
   111
    "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
paulson@23449
   112
    f \<in> pset cl \<rightarrow> pset cl" 
paulson@23449
   113
proof (neg_clausify)
paulson@23449
   114
assume 0: "(cl, f) \<in> Sigma CL llabs_subgoal_1"
paulson@23449
   115
assume 1: "\<And>cl. llabs_subgoal_1 cl =
paulson@23449
   116
     Collect
berghofe@23756
   117
      (llabs_List_Xlists_def_1_ (Pi (pset cl) (COMBK (pset cl))))"
paulson@23449
   118
assume 2: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
paulson@23449
   119
show "False"
berghofe@23756
   120
  by (metis Collect_mem_eq 1 2 SigmaD2 0)
paulson@23449
   121
qed finish_clausify
paulson@23449
   122
    (*Hack to prevent the "Additional hypotheses" error*)
paulson@23449
   123
paulson@23449
   124
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*}
paulson@23449
   125
lemma
paulson@23449
   126
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
paulson@23449
   127
   f \<in> pset cl \<inter> cl"
paulson@23449
   128
by (metis Collect_mem_eq SigmaD2)
paulson@23449
   129
paulson@23449
   130
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
paulson@23449
   131
lemma
paulson@23449
   132
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
paulson@23449
   133
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
paulson@23449
   134
by auto
paulson@23449
   135
paulson@23449
   136
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Int"*}
paulson@23449
   137
lemma "(cl,f) \<in> CLF ==> 
paulson@23449
   138
   CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
paulson@23449
   139
   f \<in> pset cl \<inter> cl"
paulson@23449
   140
by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
paulson@23449
   141
  --{*@{text Int_def} is redundant}
paulson@23449
   142
paulson@23449
   143
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
paulson@23449
   144
lemma "(cl,f) \<in> CLF ==> 
paulson@23449
   145
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
paulson@23449
   146
   f \<in> pset cl \<inter> cl"
paulson@23449
   147
by (metis Collect_mem_eq Int_commute SigmaD2)
paulson@23449
   148
paulson@23449
   149
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
paulson@23449
   150
lemma 
paulson@23449
   151
   "(cl,f) \<in> CLF ==> 
paulson@23449
   152
    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
paulson@23449
   153
    f \<in> pset cl \<rightarrow> pset cl"
paulson@23449
   154
by (metis Collect_mem_eq SigmaD2 subsetD)
paulson@23449
   155
paulson@23449
   156
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
paulson@23449
   157
lemma 
paulson@23449
   158
  "(cl,f) \<in> CLF ==> 
paulson@23449
   159
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
paulson@23449
   160
   f \<in> pset cl \<rightarrow> pset cl"
paulson@23449
   161
by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
paulson@23449
   162
paulson@23449
   163
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
paulson@23449
   164
lemma 
paulson@23449
   165
  "(cl,f) \<in> CLF ==> 
paulson@23449
   166
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
paulson@23449
   167
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
paulson@23449
   168
by auto
paulson@23449
   169
paulson@23449
   170
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipA"*}
paulson@23449
   171
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
paulson@23449
   172
apply (induct xs)
paulson@23449
   173
(*sledgehammer*)  
paulson@23449
   174
apply auto
paulson@23449
   175
done
paulson@23449
   176
paulson@23449
   177
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipB"*}
paulson@23449
   178
lemma "map (%w. (w -> w, w \<times> w)) xs = 
paulson@23449
   179
       zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
paulson@23449
   180
apply (induct xs)
paulson@23449
   181
(*sledgehammer*)  
paulson@23449
   182
apply auto
paulson@23449
   183
done
paulson@23449
   184
paulson@23449
   185
ML{*ResAtp.problem_name := "Abstraction__image_evenA"*}
paulson@23449
   186
lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)";
paulson@23449
   187
(*sledgehammer*)  
paulson@23449
   188
by auto
paulson@23449
   189
paulson@23449
   190
ML{*ResAtp.problem_name := "Abstraction__image_evenB"*}
paulson@23449
   191
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
paulson@23449
   192
       ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
paulson@23449
   193
(*sledgehammer*)  
paulson@23449
   194
by auto
paulson@23449
   195
paulson@23449
   196
ML{*ResAtp.problem_name := "Abstraction__image_curry"*}
paulson@23449
   197
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
   198
(*sledgehammer*)  
paulson@23449
   199
by auto
paulson@23449
   200
paulson@23449
   201
ML{*ResAtp.problem_name := "Abstraction__image_TimesA"*}
paulson@23449
   202
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
paulson@23449
   203
(*sledgehammer*) 
paulson@23449
   204
apply (rule equalityI)
paulson@23449
   205
(***Even the two inclusions are far too difficult
paulson@23449
   206
ML{*ResAtp.problem_name := "Abstraction__image_TimesA_simpler"*}
paulson@23449
   207
***)
paulson@23449
   208
apply (rule subsetI)
paulson@23449
   209
apply (erule imageE)
paulson@23449
   210
(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)
paulson@23449
   211
apply (erule ssubst)
paulson@23449
   212
apply (erule SigmaE)
paulson@23449
   213
(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
paulson@23449
   214
apply (erule ssubst)
paulson@23449
   215
apply (subst split_conv)
paulson@23449
   216
apply (rule SigmaI) 
paulson@23449
   217
apply (erule imageI) +
paulson@23449
   218
txt{*subgoal 2*}
paulson@23449
   219
apply (clarify );
paulson@23449
   220
apply (simp add: );  
paulson@23449
   221
apply (rule rev_image_eqI)  
paulson@23449
   222
apply (blast intro: elim:); 
paulson@23449
   223
apply (simp add: );
paulson@23449
   224
done
paulson@23449
   225
paulson@23449
   226
(*Given the difficulty of the previous problem, these two are probably
paulson@23449
   227
impossible*)
paulson@23449
   228
paulson@23449
   229
ML{*ResAtp.problem_name := "Abstraction__image_TimesB"*}
paulson@23449
   230
lemma image_TimesB:
paulson@23449
   231
    "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" 
paulson@23449
   232
(*sledgehammer*) 
paulson@23449
   233
by force
paulson@23449
   234
paulson@23449
   235
ML{*ResAtp.problem_name := "Abstraction__image_TimesC"*}
paulson@23449
   236
lemma image_TimesC:
paulson@23449
   237
    "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 
paulson@23449
   238
     ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 
paulson@23449
   239
(*sledgehammer*) 
paulson@23449
   240
by auto
paulson@23449
   241
paulson@23449
   242
end