[isabelle-dev] Current AFP problems

[Florian Haftmann]

isabelle: 03bc14eab432 tip
afp: 16e89cda027a tip

> Smooth_Manifolds FAILED
> (see also /home/haftmann/data/tum/isabelle/master/heaps/polyml-5.8_x86_64_32-linux/log/Smooth_Manifolds)
> ### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>
> ### \<Longrightarrow> closed (\<Union> ?S)
> ### Rule already declared as introduction (intro)
> ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>
> ### \<Longrightarrow> closed (\<Union> (?B ` ?A))
> ### Rule already declared as introduction (intro)
> ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)
> ### Rule already declared as introduction (intro)
> ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)
> ### Rule already declared as introduction (intro)
> ### closed ?S \<Longrightarrow> open (- ?S)
> ### Rule already declared as introduction (intro)
> ### open ?S \<Longrightarrow> closed (- ?S)
> ### Rule already declared as introduction (intro)
> ### continuous_on ?s (linepath ?a ?b)
> ### Rule already declared as introduction (intro)
> ### (\<And>i. continuous_on UNIV (\<lambda>x. ?f x i)) \<Longrightarrow>
> ### continuous_on UNIV ?f
> \<lbrakk>\<forall>x.
>             x \<in> manifold_eucl.diff_fun_space k \<longrightarrow>
>             X x \<in> UNIV;
>  \<forall>x.
>     x \<in> ?S \<longrightarrow>
>     ?g x \<in> manifold_eucl.diff_fun_space k\<rbrakk>
> \<Longrightarrow> X (\<lambda>x. \<Sum>i\<in>?S. ?g i x) =
>                   (\<Sum>a\<in>?S. X (?g a))
> locale diff
>   fixes k :: "enat"
>     and charts1 :: "('a, 'e) chart set"
>     and charts2 :: "('b, 'f) chart set"
>     and f :: "'a \<Rightarrow> 'b"
>   assumes "diff k charts1 charts2 f"
> locale c_manifold
>   fixes charts :: "('a, 'b) chart set"
>     and k :: "enat"
>   assumes "c_manifold charts k"
> ### theory "Smooth_Manifolds.Cotangent_Space"
> ### 2.370s elapsed time, 12.536s cpu time, 4.080s GC time
> *** Failed to refine any pending goal
> *** At command "by" (line 632 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
> 
> Finished HOL-Probability (0:01:16 elapsed time, 0:06:44 cpu time, factor 5.26)
> Building Randomised_Social_Choice ...
> Randomised_Social_Choice FAILED
> (see also /home/haftmann/data/tum/isabelle/master/heaps/polyml-5.8_x86_64_32-linux/log/Randomised_Social_Choice)
>        Proof.context -> Proof.state
> val parse_rat = fn: Token.T list -> Rat.rat * Token.T list
> val parse_support = fn: string list parser
> val parse_lottery = fn: (string * Rat.rat) list parser
> val pref_classes = fn: 'a list list -> 'a list list
> val combine_all = fn: ('a * 'a -> 'b) -> 'a list -> 'b list
> val prepare_strategyproofness_intro_thms = fn:
>    Proof.context ->
>      int option ->
>        thm -> Preference_Profiles_Cmd.info list -> (binding * thm list) list
> val gen_derive_strategyproofness_conditions = fn:
>    Proof.context -> int option -> thm option -> term list -> Proof.state
> val derive_strategyproofness_conditions_cmd = fn:
>    int option -> thm option -> string list -> Proof.context -> Proof.state
> ### theory "Randomised_Social_Choice.SDS_Automation"
> ### 2.607s elapsed time, 12.148s cpu time, 1.084s GC time
> ### Ignoring duplicate rewrite rule:
> ### mset (map ?f1 ?xs1) \<equiv> image_mset ?f1 (mset ?xs1)
> *** Failed to finish proof (line 462 of "$AFP/Randomised_Social_Choice/Stochastic_Dominance.thy"):
> *** goal (1 subgoal):
> ***  1. \<lbrakk>(\<Sum>a | a \<in> carrier \<and> le x a. pmf p a) +
> ***              (\<Sum>a\<in>carrier.
> ***                 \<epsilon> *
> ***                 (pmf p a * real (length xs - weak_ranking_index a)))
> ***              \<le> (\<Sum>a | a \<in> carrier \<and> le x a. pmf q a) +
> ***                    (\<Sum>a\<in>carrier.
> ***                       \<epsilon> *
> ***                       (pmf q a * real (length xs - weak_ranking_index a)));
> ***      x \<in> carrier; {y. le x y} \<subseteq> carrier\<rbrakk>
> ***     \<Longrightarrow> (\<Sum>y | le x y. pmf p y) +
> ***                       (\<Sum>n\<in>carrier.
> ***                          \<epsilon> *
> ***                          (pmf p n *
> ***                           real (length xs - weak_ranking_index n)))
> ***                       \<le> (\<Sum>y | le x y. pmf q y) +
> ***                             (\<Sum>n\<in>carrier.
> ***                                \<epsilon> *
> ***                                (pmf q n *
> ***                                 real (length xs - weak_ranking_index n)))
> *** At command "by" (line 462 of "$AFP/Randomised_Social_Choice/Stochastic_Dominance.thy")
> SDS_Impossibility CANCELLED
> Unfinished session(s): Randomised_Social_Choice, SDS_Impossibility, Smooth_Manifolds
> 0:10:29 elapsed time, 0:49:07 cpu time, factor 4.68

Cheers,
	Florian


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20190308/761c5e5f/attachment-0001.asc>