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;
wenzelm@33027
     1
(*  Title:      HOL/Metis_Examples/Abstraction.thy
paulson@23449
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
blanchet@41144
     3
    Author:     Jasmin Blanchette, TU Muenchen
paulson@23449
     4
blanchet@41144
     5
Testing Metis.
paulson@23449
     6
*)
paulson@23449
     7
haftmann@27368
     8
theory Abstraction
wenzelm@41413
     9
imports Main "~~/src/HOL/Library/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
blanchet@38991
    25
declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_triv" ]]
paulson@23449
    26
lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
blanchet@36566
    27
proof -
blanchet@36566
    28
  assume "a \<in> {x. P x}"
blanchet@36566
    29
  hence "a \<in> P" by (metis Collect_def)
blanchet@36566
    30
  hence "P a" by (metis mem_def)
blanchet@36566
    31
  thus "P a" by metis
paulson@23449
    32
qed
paulson@23449
    33
paulson@23449
    34
lemma Collect_triv: "a \<in> {x. P x} ==> P a"
berghofe@23756
    35
by (metis mem_Collect_eq)
paulson@23449
    36
paulson@23449
    37
blanchet@38991
    38
declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_mp" ]]
paulson@23449
    39
lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
blanchet@36566
    40
  by (metis Collect_imp_eq ComplD UnE)
paulson@23449
    41
blanchet@38991
    42
declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_triv" ]]
paulson@23449
    43
lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
blanchet@36566
    44
proof -
blanchet@36566
    45
  assume A1: "(a, b) \<in> Sigma A B"
blanchet@36566
    46
  hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
blanchet@36566
    47
  have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
blanchet@36566
    48
  have "b \<in> B a" by (metis F1)
blanchet@36566
    49
  thus "a \<in> A \<and> b \<in> B a" by (metis F2)
paulson@23449
    50
qed
paulson@23449
    51
paulson@23449
    52
lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
paulson@23449
    53
by (metis SigmaD1 SigmaD2)
paulson@23449
    54
blanchet@38991
    55
declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect" ]]
blanchet@36566
    56
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
blanchet@36566
    57
(* Metis says this is satisfiable!
paulson@29676
    58
by (metis CollectD SigmaD1 SigmaD2)
paulson@29676
    59
*)
paulson@23449
    60
by (meson CollectD SigmaD1 SigmaD2)
paulson@23449
    61
paulson@23449
    62
blanchet@36566
    63
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
blanchet@36566
    64
by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq)
paulson@24827
    65
blanchet@36566
    66
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
blanchet@36566
    67
proof -
blanchet@36566
    68
  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
blanchet@36566
    69
  have F1: "\<forall>u. {u} = op = u" by (metis singleton_conv2 Collect_def)
blanchet@36571
    70
  have F2: "\<forall>y w v. v \<in> w -` op = y \<longrightarrow> w v = y"
blanchet@36571
    71
    by (metis F1 vimage_singleton_eq)
blanchet@36571
    72
  have F3: "\<forall>x w. (\<lambda>R. w (x R)) = x -` w"
blanchet@36571
    73
    by (metis vimage_Collect_eq Collect_def)
blanchet@36571
    74
  show "a \<in> A \<and> a = f b" by (metis A1 F2 F3 mem_Sigma_iff Collect_def)
paulson@24827
    75
qed
paulson@24827
    76
blanchet@36566
    77
(* Alternative structured proof *)
blanchet@36566
    78
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
blanchet@36566
    79
proof -
blanchet@36566
    80
  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
blanchet@36566
    81
  hence F1: "a \<in> A" by (metis mem_Sigma_iff)
blanchet@36566
    82
  have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
blanchet@36566
    83
  hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def)
blanchet@36566
    84
  hence "a = f b" by (unfold mem_def)
blanchet@36566
    85
  thus "a \<in> A \<and> a = f b" by (metis F1)
paulson@24827
    86
qed
paulson@23449
    87
paulson@23449
    88
blanchet@38991
    89
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_in_pp" ]]
paulson@23449
    90
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
paulson@24827
    91
by (metis Collect_mem_eq SigmaD2)
paulson@23449
    92
paulson@24742
    93
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
blanchet@36566
    94
proof -
blanchet@36566
    95
  assume A1: "(cl, f) \<in> CLF"
blanchet@36566
    96
  assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
blanchet@36566
    97
  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
blanchet@36566
    98
  have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
blanchet@36566
    99
  hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def)
blanchet@36566
   100
  hence "f \<in> pset cl" by (metis A1)
blanchet@36566
   101
  thus "f \<in> pset cl" by metis
paulson@24827
   102
qed
paulson@23449
   103
blanchet@38991
   104
declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]]
paulson@23449
   105
lemma
paulson@23449
   106
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
paulson@23449
   107
    f \<in> pset cl \<rightarrow> pset cl"
blanchet@36566
   108
proof -
blanchet@36566
   109
  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
blanchet@36566
   110
  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
blanchet@36566
   111
  have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
blanchet@36566
   112
  hence "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
blanchet@36566
   113
  thus "f \<in> pset cl \<rightarrow> pset cl" by metis
paulson@24827
   114
qed
paulson@23449
   115
blanchet@38991
   116
declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Int" ]]
paulson@23449
   117
lemma
paulson@23449
   118
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
paulson@23449
   119
   f \<in> pset cl \<inter> cl"
blanchet@36566
   120
proof -
blanchet@36566
   121
  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
blanchet@36566
   122
  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
blanchet@36566
   123
  have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
blanchet@36566
   124
  hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def)
blanchet@36566
   125
  hence "f \<in> Id_on cl `` pset cl" by metis
blanchet@36566
   126
  hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
blanchet@36566
   127
  thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
paulson@24827
   128
qed
paulson@24827
   129
paulson@23449
   130
blanchet@38991
   131
declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi_mono" ]]
paulson@23449
   132
lemma
paulson@23449
   133
    "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
paulson@23449
   134
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
paulson@23449
   135
by auto
paulson@23449
   136
blanchet@38991
   137
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Int" ]]
paulson@23449
   138
lemma "(cl,f) \<in> CLF ==> 
paulson@23449
   139
   CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
paulson@23449
   140
   f \<in> pset cl \<inter> cl"
paulson@24827
   141
by auto
haftmann@27368
   142
paulson@23449
   143
blanchet@38991
   144
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]]
paulson@23449
   145
lemma "(cl,f) \<in> CLF ==> 
paulson@23449
   146
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
paulson@23449
   147
   f \<in> pset cl \<inter> cl"
paulson@24827
   148
by auto
blanchet@36566
   149
paulson@23449
   150
blanchet@38991
   151
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]]
paulson@23449
   152
lemma 
paulson@23449
   153
   "(cl,f) \<in> CLF ==> 
paulson@23449
   154
    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
paulson@23449
   155
    f \<in> pset cl \<rightarrow> pset cl"
nipkow@31754
   156
by fast
blanchet@36566
   157
paulson@23449
   158
blanchet@38991
   159
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]]
paulson@23449
   160
lemma 
paulson@23449
   161
  "(cl,f) \<in> CLF ==> 
paulson@23449
   162
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
paulson@23449
   163
   f \<in> pset cl \<rightarrow> pset cl"
paulson@24827
   164
by auto
blanchet@36566
   165
paulson@23449
   166
blanchet@38991
   167
declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]]
paulson@23449
   168
lemma 
paulson@23449
   169
  "(cl,f) \<in> CLF ==> 
paulson@23449
   170
   CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
paulson@23449
   171
   (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
paulson@23449
   172
by auto
paulson@23449
   173
blanchet@38991
   174
declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipA" ]]
paulson@23449
   175
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
paulson@23449
   176
apply (induct xs)
blanchet@36566
   177
 apply (metis map_is_Nil_conv zip.simps(1))
blanchet@36566
   178
by auto
paulson@23449
   179
blanchet@38991
   180
declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipB" ]]
paulson@23449
   181
lemma "map (%w. (w -> w, w \<times> w)) xs = 
paulson@23449
   182
       zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
paulson@23449
   183
apply (induct xs)
blanchet@36566
   184
 apply (metis Nil_is_map_conv zip_Nil)
blanchet@36566
   185
by auto
paulson@23449
   186
blanchet@38991
   187
declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenA" ]]
blanchet@36566
   188
lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)"
blanchet@36566
   189
by (metis Collect_def image_subset_iff mem_def)
paulson@23449
   190
blanchet@38991
   191
declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenB" ]]
paulson@23449
   192
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
paulson@23449
   193
       ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
blanchet@36566
   194
by (metis Collect_def imageI image_image image_subset_iff mem_def)
paulson@23449
   195
blanchet@38991
   196
declare [[ sledgehammer_problem_prefix = "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)" 
blanchet@36566
   198
(*sledgehammer*)
paulson@23449
   199
by auto
paulson@23449
   200
blanchet@38991
   201
declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesA" ]]
paulson@23449
   202
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
blanchet@36566
   203
(*sledgehammer*)
paulson@23449
   204
apply (rule equalityI)
paulson@23449
   205
(***Even the two inclusions are far too difficult
blanchet@38991
   206
using [[ sledgehammer_problem_prefix = "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
blanchet@38991
   229
declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesB" ]]
paulson@23449
   230
lemma image_TimesB:
blanchet@36566
   231
    "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
blanchet@36566
   232
(*sledgehammer*)
paulson@23449
   233
by force
paulson@23449
   234
blanchet@38991
   235
declare [[ sledgehammer_problem_prefix = "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)" 
blanchet@36566
   239
(*sledgehammer*)
paulson@23449
   240
by auto
paulson@23449
   241
paulson@23449
   242
end