23449

1 
(* Title: HOL/MetisExamples/Abstraction.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 


5 
Testing the metis method


6 
*)


7 


8 
theory Abstraction imports FuncSet


9 
begin


10 


11 
(*For Christoph Benzmueller*)


12 
lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";


13 
by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)


14 


15 
(*this is a theorem, but we can't prove it unless ext is applied explicitly


16 
lemma "(op=) = (%x y. y=x)"


17 
*)


18 


19 
consts


20 
monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"


21 
pset :: "'a set => 'a set"


22 
order :: "'a set => ('a * 'a) set"


23 


24 
ML{*ResAtp.problem_name := "Abstraction__Collect_triv"*}


25 
lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"


26 
proof (neg_clausify)


27 
assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"


28 
assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"


29 
have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"


30 
by (metis CollectD 0)


31 
show "False"


32 
by (metis 2 1)


33 
qed


34 


35 
lemma Collect_triv: "a \<in> {x. P x} ==> P a"


36 
by (metis member_Collect_eq member_def)


37 


38 


39 
ML{*ResAtp.problem_name := "Abstraction__Collect_mp"*}


40 
lemma "a \<in> {x. P x > Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"


41 
by (metis CollectI Collect_imp_eq ComplD UnE memberI member_Collect_eq);


42 
{*34 secs*}


43 


44 
ML{*ResAtp.problem_name := "Abstraction__Sigma_triv"*}


45 
lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"


46 
proof (neg_clausify)


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)"


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"


49 
have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"


50 
by (metis SigmaD1 0)


51 
have 3: "(b\<Colon>'b\<Colon>type) \<in> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"


52 
by (metis SigmaD2 0)


53 
have 4: "(b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"


54 
by (metis 1 2)


55 
show "False"


56 
by (metis 3 4)


57 
qed


58 


59 
lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"


60 
by (metis SigmaD1 SigmaD2)


61 


62 
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect"*}


63 
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"


64 
(*???metis cannot prove this


65 
by (metis CollectD SigmaD1 SigmaD2 UN_eq)


66 
Also, UN_eq is unnecessary*)


67 
by (meson CollectD SigmaD1 SigmaD2)


68 


69 


70 


71 
(*singlestep*)


72 
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"


73 
proof (neg_clausify)


74 
assume 0: "(a, b) \<in> Sigma A (llabs_subgoal_1 f)"


75 
assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"


76 
assume 2: "a \<notin> A \<or> a \<noteq> f b"


77 
have 3: "a \<in> A"


78 
by (metis SigmaD1 0)


79 
have 4: "b \<in> llabs_subgoal_1 f a"


80 
by (metis SigmaD2 0)


81 
have 5: "\<And>X1 X2. X2 ` {X1} = llabs_subgoal_1 X2 X1"


82 
by (metis 1 vimage_Collect_eq singleton_conv2)


83 
have 6: "\<And>X1 X2 X3. X1 X2 = X3 \<or> X2 \<notin> llabs_subgoal_1 X1 X3"


84 
by (metis vimage_singleton_eq 5)


85 
have 7: "f b \<noteq> a"


86 
by (metis 2 3)


87 
have 8: "f b = a"


88 
by (metis 6 4)


89 
show "False"


90 
by (metis 8 7)


91 
qed finish_clausify


92 


93 


94 
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*}


95 
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"


96 
apply (metis Collect_mem_eq SigmaD2);


97 
done


98 


99 
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"proof (neg_clausify)


100 
assume 0: "(cl, f) \<in> CLF"


101 
assume 1: "CLF = Sigma CL llabs_subgoal_1"


102 
assume 2: "\<And>cl. llabs_subgoal_1 cl =


103 
Collect (llabs_Predicate_XRangeP_def_2_ op \<in> (pset cl))"


104 
assume 3: "f \<notin> pset cl"


105 
show "False"


106 
by (metis 0 1 SigmaD2 3 2 Collect_mem_eq)


107 
qed finish_clausify (*ugly hack: combinators??*)


108 


109 
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}


110 
lemma


111 
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>


112 
f \<in> pset cl \<rightarrow> pset cl"


113 
apply (metis Collect_mem_eq SigmaD2);


114 
done


115 


116 
lemma


117 
"(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>


118 
f \<in> pset cl \<rightarrow> pset cl"


119 
proof (neg_clausify)


120 
assume 0: "(cl, f) \<in> Sigma CL llabs_subgoal_1"


121 
assume 1: "\<And>cl. llabs_subgoal_1 cl =


122 
Collect


123 
(llabs_Predicate_XRangeP_def_2_ op \<in> (Pi (pset cl) (COMBK (pset cl))))"


124 
assume 2: "f \<notin> Pi (pset cl) (COMBK (pset cl))"


125 
show "False"


126 
by (metis Collect_mem_eq 1 2 SigmaD2 0 member2_def)


127 
qed finish_clausify


128 
(*Hack to prevent the "Additional hypotheses" error*)


129 


130 
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*}


131 
lemma


132 
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>


133 
f \<in> pset cl \<inter> cl"


134 
by (metis Collect_mem_eq SigmaD2)


135 


136 
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}


137 
lemma


138 
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>


139 
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"


140 
by auto


141 


142 
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Int"*}


143 
lemma "(cl,f) \<in> CLF ==>


144 
CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>


145 
f \<in> pset cl \<inter> cl"


146 
by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)


147 
{*@{text Int_def} is redundant}


148 


149 
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}


150 
lemma "(cl,f) \<in> CLF ==>


151 
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>


152 
f \<in> pset cl \<inter> cl"


153 
by (metis Collect_mem_eq Int_commute SigmaD2)


154 


155 
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}


156 
lemma


157 
"(cl,f) \<in> CLF ==>


158 
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==>


159 
f \<in> pset cl \<rightarrow> pset cl"


160 
by (metis Collect_mem_eq SigmaD2 subsetD)


161 


162 
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}


163 
lemma


164 
"(cl,f) \<in> CLF ==>


165 
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>


166 
f \<in> pset cl \<rightarrow> pset cl"


167 
by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)


168 


169 
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}


170 
lemma


171 
"(cl,f) \<in> CLF ==>


172 
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>


173 
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"


174 
by auto


175 


176 
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipA"*}


177 
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"


178 
apply (induct xs)


179 
(*sledgehammer*)


180 
apply auto


181 
done


182 


183 
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipB"*}


184 
lemma "map (%w. (w > w, w \<times> w)) xs =


185 
zip (map (%w. w > w) xs) (map (%w. w \<times> w) xs)"


186 
apply (induct xs)


187 
(*sledgehammer*)


188 
apply auto


189 
done


190 


191 
ML{*ResAtp.problem_name := "Abstraction__image_evenA"*}


192 
lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x > Suc(f x) \<in> A)";


193 
(*sledgehammer*)


194 
by auto


195 


196 
ML{*ResAtp.problem_name := "Abstraction__image_evenB"*}


197 
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A


198 
==> (\<forall>x. even x > f (f (Suc(f x))) \<in> A)";


199 
(*sledgehammer*)


200 
by auto


201 


202 
ML{*ResAtp.problem_name := "Abstraction__image_curry"*}


203 
lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)"


204 
(*sledgehammer*)


205 
by auto


206 


207 
ML{*ResAtp.problem_name := "Abstraction__image_TimesA"*}


208 
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"


209 
(*sledgehammer*)


210 
apply (rule equalityI)


211 
(***Even the two inclusions are far too difficult


212 
ML{*ResAtp.problem_name := "Abstraction__image_TimesA_simpler"*}


213 
***)


214 
apply (rule subsetI)


215 
apply (erule imageE)


216 
(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)


217 
apply (erule ssubst)


218 
apply (erule SigmaE)


219 
(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)


220 
apply (erule ssubst)


221 
apply (subst split_conv)


222 
apply (rule SigmaI)


223 
apply (erule imageI) +


224 
txt{*subgoal 2*}


225 
apply (clarify );


226 
apply (simp add: );


227 
apply (rule rev_image_eqI)


228 
apply (blast intro: elim:);


229 
apply (simp add: );


230 
done


231 


232 
(*Given the difficulty of the previous problem, these two are probably


233 
impossible*)


234 


235 
ML{*ResAtp.problem_name := "Abstraction__image_TimesB"*}


236 
lemma image_TimesB:


237 
"(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"


238 
(*sledgehammer*)


239 
by force


240 


241 
ML{*ResAtp.problem_name := "Abstraction__image_TimesC"*}


242 
lemma image_TimesC:


243 
"(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =


244 
((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)"


245 
(*sledgehammer*)


246 
by auto


247 


248 
end
