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