src/HOL/MetisExamples/Abstraction.thy
 author paulson Thu Sep 27 17:55:28 2007 +0200 (2007-09-27) changeset 24742 73b8b42a36b6 parent 24632 779fc4fcbf8b child 24783 5a3e336a2e37 permissions -rw-r--r--
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
theorems of Nat.thy are hidden by the Ordering.thy versions
 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 \ {x. P x} ==> P a" ``` paulson@23449 ` 26` ```proof (neg_clausify) ``` paulson@23449 ` 27` ```assume 0: "(a\'a\type) \ Collect (P\'a\type \ bool)" ``` paulson@23449 ` 28` ```assume 1: "\ (P\'a\type \ bool) (a\'a\type)" ``` paulson@23449 ` 29` ```have 2: "(P\'a\type \ bool) (a\'a\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 \ {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 \ {x. P x --> Q x} ==> a \ {x. P x} ==> a \ {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) \ Sigma A B ==> a \ A & b \ B a" ``` paulson@23449 ` 46` ```proof (neg_clausify) ``` paulson@23449 ` 47` ```assume 0: "(a\'a\type, b\'b\type) \ Sigma (A\'a\type set) (B\'a\type \ 'b\type set)" ``` paulson@23449 ` 48` ```assume 1: "(a\'a\type) \ (A\'a\type set) \ (b\'b\type) \ (B\'a\type \ 'b\type set) a" ``` paulson@23449 ` 49` ```have 2: "(a\'a\type) \ (A\'a\type set)" ``` paulson@23449 ` 50` ``` by (metis SigmaD1 0) ``` paulson@23449 ` 51` ```have 3: "(b\'b\type) \ (B\'a\type \ 'b\type set) (a\'a\type)" ``` paulson@23449 ` 52` ``` by (metis SigmaD2 0) ``` paulson@23449 ` 53` ```have 4: "(b\'b\type) \ (B\'a\type \ 'b\type set) (a\'a\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) \ Sigma A B ==> a \ A & b \ 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) \ (SIGMA x: A. {y. x = f y}) ==> a \ 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) \ (SIGMA x: A. {y. x = f y}) ==> a \ A & a = f b" ``` paulson@23449 ` 73` ```proof (neg_clausify) ``` paulson@23449 ` 74` ```assume 0: "(a, b) \ Sigma A (llabs_subgoal_1 f)" ``` paulson@23449 ` 75` ```assume 1: "\f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)" ``` paulson@23449 ` 76` ```assume 2: "a \ A \ a \ f b" ``` paulson@23449 ` 77` ```have 3: "a \ A" ``` berghofe@23756 ` 78` ``` by (metis SigmaD1 0) ``` paulson@23519 ` 79` ```have 4: "f b \ 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) \ CLF ==> CLF = (SIGMA cl: CL.{f. f \ pset cl}) ==> f \ pset cl" ``` paulson@23449 ` 90` ```apply (metis Collect_mem_eq SigmaD2); ``` paulson@23449 ` 91` ```done ``` paulson@23449 ` 92` paulson@24742 ` 93` ```lemma "(cl,f) \ CLF ==> CLF = (SIGMA cl: CL.{f. f \ pset cl}) ==> f \ pset cl" ``` paulson@24742 ` 94` ```proof (neg_clausify) ``` paulson@24742 ` 95` ```assume 0: "\cl\'a\type set. ``` paulson@24742 ` 96` ``` (llabs_subgoal_1\'a\type set \ 'a\type set) cl = ``` paulson@24742 ` 97` ``` Collect (llabs_Set_XCollect_ex_eq_3_ op \ (pset cl))" ``` paulson@24742 ` 98` ```assume 1: "(f\'a\type) \ pset (cl\'a\type set)" ``` paulson@24742 ` 99` ```assume 2: "(cl\'a\type set, f\'a\type) \ (CLF\('a\type set \ 'a\type) set)" ``` paulson@24742 ` 100` ```have 3: "llabs_Predicate_Xsup_Un_eq2_1_ (CLF\('a\type set \ 'a\type) set) ``` paulson@24742 ` 101` ``` (cl\'a\type set) (f\'a\type)" ``` paulson@24742 ` 102` ``` by (metis acc_def 2) ``` paulson@24742 ` 103` ```assume 4: "(CLF\('a\type set \ 'a\type) set) = ``` paulson@24742 ` 104` ```Sigma (CL\'a\type set set) (llabs_subgoal_1\'a\type set \ 'a\type set)" ``` paulson@23449 ` 105` ```show "False" ``` paulson@24742 ` 106` ``` by (metis 1 Collect_mem_eq 0 3 4 acc_def SigmaD2) ``` paulson@23449 ` 107` ```qed finish_clausify (*ugly hack: combinators??*) ``` paulson@23449 ` 108` paulson@23449 ` 109` ```ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*} ``` paulson@23449 ` 110` ```lemma ``` paulson@23449 ` 111` ``` "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> ``` paulson@23449 ` 112` ``` f \ pset cl \ pset cl" ``` paulson@23449 ` 113` ```apply (metis Collect_mem_eq SigmaD2); ``` paulson@23449 ` 114` ```done ``` paulson@23449 ` 115` paulson@23449 ` 116` ```lemma ``` paulson@23449 ` 117` ``` "(cl,f) \ (SIGMA cl::'a set : CL. {f. f \ pset cl \ pset cl}) ==> ``` paulson@24632 ` 118` ``` f \ pset cl \ pset cl" ``` paulson@23449 ` 119` ```proof (neg_clausify) ``` paulson@24742 ` 120` ```assume 0: "\cl\'a\type set. ``` paulson@24742 ` 121` ``` (llabs_subgoal_1\'a\type set \ ('a\type \ 'a\type) set) cl = ``` paulson@24742 ` 122` ``` Collect ``` paulson@24742 ` 123` ``` (llabs_Set_XCollect_ex_eq_3_ op \ (Pi (pset cl) (COMBK (pset cl))))" ``` paulson@24742 ` 124` ```assume 1: "(f\'a\type \ 'a\type) \ Pi (pset (cl\'a\type set)) (COMBK (pset cl))" ``` paulson@24742 ` 125` ```assume 2: "(cl\'a\type set, f\'a\type \ 'a\type) ``` paulson@24742 ` 126` ```\ Sigma (CL\'a\type set set) ``` paulson@24742 ` 127` ``` (llabs_subgoal_1\'a\type set \ ('a\type \ 'a\type) set)" ``` paulson@23449 ` 128` ```show "False" ``` paulson@24742 ` 129` ``` by (metis 1 Collect_mem_eq 0 SigmaD2 2) ``` paulson@23449 ` 130` ```qed finish_clausify ``` paulson@23449 ` 131` ``` (*Hack to prevent the "Additional hypotheses" error*) ``` paulson@23449 ` 132` paulson@23449 ` 133` ```ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*} ``` paulson@23449 ` 134` ```lemma ``` paulson@23449 ` 135` ``` "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> ``` paulson@23449 ` 136` ``` f \ pset cl \ cl" ``` paulson@23449 ` 137` ```by (metis Collect_mem_eq SigmaD2) ``` paulson@23449 ` 138` paulson@23449 ` 139` ```ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*} ``` paulson@23449 ` 140` ```lemma ``` paulson@23449 ` 141` ``` "(cl,f) \ (SIGMA cl: CL. {f. f \ pset cl \ pset cl & monotone f (pset cl) (order cl)}) ==> ``` paulson@23449 ` 142` ``` (f \ pset cl \ pset cl) & (monotone f (pset cl) (order cl))" ``` paulson@23449 ` 143` ```by auto ``` paulson@23449 ` 144` paulson@23449 ` 145` ```ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Int"*} ``` paulson@23449 ` 146` ```lemma "(cl,f) \ CLF ==> ``` paulson@23449 ` 147` ``` CLF \ (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> ``` paulson@23449 ` 148` ``` f \ pset cl \ cl" ``` paulson@23449 ` 149` ```by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1) ``` paulson@23449 ` 150` ``` --{*@{text Int_def} is redundant} ``` paulson@23449 ` 151` paulson@23449 ` 152` ```ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*} ``` paulson@23449 ` 153` ```lemma "(cl,f) \ CLF ==> ``` paulson@23449 ` 154` ``` CLF = (SIGMA cl: CL. {f. f \ pset cl \ cl}) ==> ``` paulson@23449 ` 155` ``` f \ pset cl \ cl" ``` paulson@23449 ` 156` ```by (metis Collect_mem_eq Int_commute SigmaD2) ``` paulson@23449 ` 157` paulson@23449 ` 158` ```ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*} ``` paulson@23449 ` 159` ```lemma ``` paulson@23449 ` 160` ``` "(cl,f) \ CLF ==> ``` paulson@23449 ` 161` ``` CLF \ (SIGMA cl': CL. {f. f \ pset cl' \ pset cl'}) ==> ``` paulson@23449 ` 162` ``` f \ pset cl \ pset cl" ``` paulson@23449 ` 163` ```by (metis Collect_mem_eq SigmaD2 subsetD) ``` paulson@23449 ` 164` paulson@23449 ` 165` ```ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*} ``` paulson@23449 ` 166` ```lemma ``` paulson@23449 ` 167` ``` "(cl,f) \ CLF ==> ``` paulson@23449 ` 168` ``` CLF = (SIGMA cl: CL. {f. f \ pset cl \ pset cl}) ==> ``` paulson@23449 ` 169` ``` f \ pset cl \ pset cl" ``` paulson@23449 ` 170` ```by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE) ``` paulson@23449 ` 171` paulson@23449 ` 172` ```ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*} ``` paulson@23449 ` 173` ```lemma ``` paulson@23449 ` 174` ``` "(cl,f) \ CLF ==> ``` paulson@23449 ` 175` ``` CLF = (SIGMA cl: CL. {f. f \ pset cl \ pset cl & monotone f (pset cl) (order cl)}) ==> ``` paulson@23449 ` 176` ``` (f \ pset cl \ pset cl) & (monotone f (pset cl) (order cl))" ``` paulson@23449 ` 177` ```by auto ``` paulson@23449 ` 178` paulson@23449 ` 179` ```ML{*ResAtp.problem_name := "Abstraction__map_eq_zipA"*} ``` paulson@23449 ` 180` ```lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)" ``` paulson@23449 ` 181` ```apply (induct xs) ``` paulson@23449 ` 182` ```(*sledgehammer*) ``` paulson@23449 ` 183` ```apply auto ``` paulson@23449 ` 184` ```done ``` paulson@23449 ` 185` paulson@23449 ` 186` ```ML{*ResAtp.problem_name := "Abstraction__map_eq_zipB"*} ``` paulson@23449 ` 187` ```lemma "map (%w. (w -> w, w \ w)) xs = ``` paulson@23449 ` 188` ``` zip (map (%w. w -> w) xs) (map (%w. w \ w) xs)" ``` paulson@23449 ` 189` ```apply (induct xs) ``` paulson@23449 ` 190` ```(*sledgehammer*) ``` paulson@23449 ` 191` ```apply auto ``` paulson@23449 ` 192` ```done ``` paulson@23449 ` 193` paulson@23449 ` 194` ```ML{*ResAtp.problem_name := "Abstraction__image_evenA"*} ``` paulson@23449 ` 195` ```lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\x. even x --> Suc(f x) \ A)"; ``` paulson@23449 ` 196` ```(*sledgehammer*) ``` paulson@23449 ` 197` ```by auto ``` paulson@23449 ` 198` paulson@23449 ` 199` ```ML{*ResAtp.problem_name := "Abstraction__image_evenB"*} ``` paulson@23449 ` 200` ```lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A ``` paulson@23449 ` 201` ``` ==> (\x. even x --> f (f (Suc(f x))) \ A)"; ``` paulson@23449 ` 202` ```(*sledgehammer*) ``` paulson@23449 ` 203` ```by auto ``` paulson@23449 ` 204` paulson@23449 ` 205` ```ML{*ResAtp.problem_name := "Abstraction__image_curry"*} ``` paulson@23449 ` 206` ```lemma "f \ (%u v. b \ u \ v) ` A ==> \u v. P (b \ u \ v) ==> P(f y)" ``` paulson@23449 ` 207` ```(*sledgehammer*) ``` paulson@23449 ` 208` ```by auto ``` paulson@23449 ` 209` paulson@23449 ` 210` ```ML{*ResAtp.problem_name := "Abstraction__image_TimesA"*} ``` paulson@23449 ` 211` ```lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \ B) = (f`A) \ (g`B)" ``` paulson@23449 ` 212` ```(*sledgehammer*) ``` paulson@23449 ` 213` ```apply (rule equalityI) ``` paulson@23449 ` 214` ```(***Even the two inclusions are far too difficult ``` paulson@23449 ` 215` ```ML{*ResAtp.problem_name := "Abstraction__image_TimesA_simpler"*} ``` paulson@23449 ` 216` ```***) ``` paulson@23449 ` 217` ```apply (rule subsetI) ``` paulson@23449 ` 218` ```apply (erule imageE) ``` paulson@23449 ` 219` ```(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*) ``` paulson@23449 ` 220` ```apply (erule ssubst) ``` paulson@23449 ` 221` ```apply (erule SigmaE) ``` paulson@23449 ` 222` ```(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*) ``` paulson@23449 ` 223` ```apply (erule ssubst) ``` paulson@23449 ` 224` ```apply (subst split_conv) ``` paulson@23449 ` 225` ```apply (rule SigmaI) ``` paulson@23449 ` 226` ```apply (erule imageI) + ``` paulson@23449 ` 227` ```txt{*subgoal 2*} ``` paulson@23449 ` 228` ```apply (clarify ); ``` paulson@23449 ` 229` ```apply (simp add: ); ``` paulson@23449 ` 230` ```apply (rule rev_image_eqI) ``` paulson@23449 ` 231` ```apply (blast intro: elim:); ``` paulson@23449 ` 232` ```apply (simp add: ); ``` paulson@23449 ` 233` ```done ``` paulson@23449 ` 234` paulson@23449 ` 235` ```(*Given the difficulty of the previous problem, these two are probably ``` paulson@23449 ` 236` ```impossible*) ``` paulson@23449 ` 237` paulson@23449 ` 238` ```ML{*ResAtp.problem_name := "Abstraction__image_TimesB"*} ``` paulson@23449 ` 239` ```lemma image_TimesB: ``` paulson@23449 ` 240` ``` "(%(x,y,z). (f x, g y, h z)) ` (A \ B \ C) = (f`A) \ (g`B) \ (h`C)" ``` paulson@23449 ` 241` ```(*sledgehammer*) ``` paulson@23449 ` 242` ```by force ``` paulson@23449 ` 243` paulson@23449 ` 244` ```ML{*ResAtp.problem_name := "Abstraction__image_TimesC"*} ``` paulson@23449 ` 245` ```lemma image_TimesC: ``` paulson@23449 ` 246` ``` "(%(x,y). (x \ x, y \ y)) ` (A \ B) = ``` paulson@23449 ` 247` ``` ((%x. x \ x) ` A) \ ((%y. y \ y) ` B)" ``` paulson@23449 ` 248` ```(*sledgehammer*) ``` paulson@23449 ` 249` ```by auto ``` paulson@23449 ` 250` paulson@23449 ` 251` ```end ```