Loading theory "Randomised_Social_Choice.QSOpt_Exact" (required by "Randomised_Social_Choice.SDS_Automation")
Loading theory "Randomised_Social_Choice.Lotteries" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes" via "Randomised_Social_Choice.Stochastic_Dominance")
Loading theory "List-Index.List_Index" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes" via "Randomised_Social_Choice.Preference_Profiles" via "Randomised_Social_Choice.Order_Predicates")
consts
  find_index ::
    "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
signature RAT_UTILS =
  sig
    val dest_rat_number: term -> Rat.rat
    val mk_rat_number: typ -> Rat.rat -> term
    val pretty_rat: Rat.rat -> string
    val rat_to_string: Rat.rat -> string
    val string_to_rat: string -> Rat.rat option
  end
structure Rat_Utils: RAT_UTILS
### theory "Randomised_Social_Choice.Lotteries"
### 0.157s elapsed time, 0.540s cpu time, 0.000s GC time
signature LP_PARAMS =
  sig
    type T
    val compare: T * T -> order
    val from_int: int -> T
    val negate: T -> T
    val print: T -> string
    val read: string -> T option
  end
signature LINEAR_PROGRAM_COMMON =
  sig
    exception QSOpt_Parse
    type 'a bound = 'a infty * var * 'a infty
    datatype comparison = EQ | GEQ | LEQ
    type 'a constraint = 'a linterm * comparison * 'a
    val gen_print_bound: ('a -> string) -> 'a bound -> string
    val gen_print_constraint:
       ('a * 'a -> order) * (int -> 'a) * ('a -> string) * ('a -> 'a) ->
         'a constraint -> string
    val gen_print_linterm:
       ('a * 'a -> order) * (int -> 'a) * ('a -> string) * ('a -> 'a) ->
         'a linterm -> string
    val gen_print_program:
       ('a * 'a -> order) * (int -> 'a) * ('a -> string) * ('a -> 'a) ->
         'a prog -> string
    val gen_read_result: (string -> 'a option) -> string -> 'a result
    datatype 'a infty = Finite of 'a | Neg_Infty | Pos_Infty
    val is_finite: 'a infty -> bool
    type 'a linterm = ('a * var) list
    val map_infty: ('a -> 'b) -> 'a infty -> 'b infty
    datatype optimization_mode = MAXIMIZE | MINIMIZE
    val print_comparison: comparison -> string
    val print_infty: ('a -> string) -> 'a infty -> string
    val print_optimization_mode: optimization_mode -> string
    type 'a prog =
       optimization_mode * 'a linterm * 'a constraint list * 'a bound list
    datatype 'a result
    = Infeasible | Optimal of 'a * (string * 'a) list | Unbounded | Unknown
    eqtype var
  end
signature LINEAR_PROGRAM =
  sig
    exception QSOpt_Parse
    type T
    type 'a bound = 'a infty * var * 'a infty
    datatype comparison = EQ | GEQ | LEQ
    type 'a constraint = 'a linterm * comparison * 'a
    val gen_print_bound: ('a -> string) -> 'a bound -> string
    val gen_print_constraint:
       ('a * 'a -> order) * (int -> 'a) * ('a -> string) * ('a -> 'a) ->
         'a constraint -> string
    val gen_print_linterm:
       ('a * 'a -> order) * (int -> 'a) * ('a -> string) * ('a -> 'a) ->
         'a linterm -> string
    val gen_print_program:
       ('a * 'a -> order) * (int -> 'a) * ('a -> string) * ('a -> 'a) ->
         'a prog -> string
    val gen_read_result: (string -> 'a option) -> string -> 'a result
    datatype 'a infty = Finite of 'a | Neg_Infty | Pos_Infty
    val is_finite: 'a infty -> bool
    type 'a linterm = ('a * var) list
    val map_infty: ('a -> 'b) -> 'a infty -> 'b infty
    datatype optimization_mode = MAXIMIZE | MINIMIZE
    val print_bound: T bound -> string
    val print_comparison: comparison -> string
    val print_constraint: T constraint -> string
    val print_infty: ('a -> string) -> 'a infty -> string
    val print_linterm: T linterm -> string
    val print_optimization_mode: optimization_mode -> string
    val print_program: T prog -> string
    type 'a prog =
       optimization_mode * 'a linterm * 'a constraint list * 'a bound list
    val read_result: string -> T result
    val read_result_file: string -> T result
    datatype 'a result
    = Infeasible | Optimal of 'a * (string * 'a) list | Unbounded | Unknown
    val save_program: string -> T prog -> unit
    val solve_program: T prog -> T result
    eqtype var
  end
structure Linear_Program_Common: LINEAR_PROGRAM_COMMON
structure Rat_Linear_Program: LINEAR_PROGRAM
functor Linear_Program (LP_Params: LP_PARAMS): LINEAR_PROGRAM
### theory "Randomised_Social_Choice.QSOpt_Exact"
### 0.321s elapsed time, 1.192s cpu time, 0.000s GC time
consts
  map_index' ::
    "nat
     \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'b)
                   \<Rightarrow> 'a list \<Rightarrow> 'b list"
consts
  insert_nth ::
    "nat \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "List-Index.List_Index"
### 1.085s elapsed time, 4.100s cpu time, 0.000s GC time
Loading theory "Randomised_Social_Choice.Order_Predicates" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes" via "Randomised_Social_Choice.Preference_Profiles")
locale preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "Order_Predicates.preorder_on carrier le"
locale total_preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "total_preorder_on carrier le"
locale preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "Order_Predicates.preorder_on carrier le"
locale order_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "order_on carrier le"
locale linorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "linorder_on carrier le"
locale preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "Order_Predicates.preorder_on carrier le"
locale total_preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "total_preorder_on carrier le"
Proofs for inductive predicate(s) "of_weak_ranking"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### Not an equation, in theorem:
### is_weak_ranking []
### Not an equation, in theorem:
### is_finite_weak_ranking []
consts
  is_weak_ranking_aux ::
    "'a set \<Rightarrow> 'a set list \<Rightarrow> bool"
### Code generator: dropping subsumed code equation
### is_weak_ranking (?x # ?xs) \<equiv>
### ?x \<noteq> {} \<and>
### is_weak_ranking ?xs \<and> ?x \<inter> \<Union> (set ?xs) = {}
"R b a = R b a"
  :: "bool"
locale finite_total_preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "finite_total_preorder_on carrier le"
locale finite_linorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "finite_linorder_on carrier le"
### theory "Randomised_Social_Choice.Order_Predicates"
### 1.655s elapsed time, 6.088s cpu time, 0.140s GC time
Loading theory "Randomised_Social_Choice.Preference_Profiles" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes")
locale preorder_family
  fixes dom :: "'a set"
    and carrier :: "'b set"
    and R :: "'a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> bool"
  assumes "preorder_family dom carrier R"
locale pref_profile_wf
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_wf agents alts R"
locale preorder_family
  fixes dom :: "'a set"
    and carrier :: "'b set"
    and R :: "'a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> bool"
  assumes "preorder_family dom carrier R"
locale pref_profile_wf
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_wf agents alts R"
locale pref_profile_wf
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_wf agents alts R"
locale pref_profile_unique_favorites
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_unique_favorites agents alts R"
### theory "Randomised_Social_Choice.Preference_Profiles"
### 1.002s elapsed time, 3.728s cpu time, 0.272s GC time
Loading theory "Randomised_Social_Choice.Elections" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes")
Loading theory "Randomised_Social_Choice.Utility_Functions" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes" via "Randomised_Social_Choice.Stochastic_Dominance")
locale election
  fixes agents :: "'agent set"
    and alts :: "'alt set"
  assumes "election agents alts"
### theory "Randomised_Social_Choice.Elections"
### 0.078s elapsed time, 0.316s cpu time, 0.000s GC time
Loading theory "Randomised_Social_Choice.Preference_Profile_Cmd" (required by "Randomised_Social_Choice.SDS_Automation")
signature PREFERENCE_PROFILES =
  sig
    val agentT: profile -> typ
    val agents_of_profile: profile -> term list
    val altT: profile -> typ
    val alts_of_profile: profile -> term list
    val apply_permutation: ('a * 'a -> bool) -> 'a permutation -> 'a -> 'a
    val apply_reverse_permutation:
       ('a * 'a -> bool) -> 'a permutation -> 'a -> 'a
    val cycles: ('a * 'a -> bool) -> 'a permutation -> 'a list list
    val derive_orbit_equations:
       profile -> ((term * term) * term permutation) list
    val eq_prefs: prefs * prefs -> bool
    val equiv_profile_anonymity: profile * profile -> bool
    val find_an_automorphisms:
       profile -> ((term * term) * term permutation) list
    val find_an_isomorphism: profile * profile -> term permutation option
    val find_an_isomorphisms: profile * profile -> term permutation Seq.seq
    val find_manipulations:
       profile * profile -> (term * term * int * term permutation) list
    val find_pareto_witness: profile -> term -> (term * term * term) option
    val fixpoints: ('a * 'a -> bool) -> 'a permutation -> 'a list
    val is_identity: ('a * 'a -> bool) -> 'a permutation -> bool
    val manipulation_distance: prefs * prefs -> int
    val pareto: profile -> term * term -> bool
    val pareto_losers: profile -> (term * term * term) list
    val pareto_pairs: profile -> (term * term * term) list
    type 'a permutation
    val permutations: ('a * 'a -> bool) -> 'a list -> 'a permutation Seq.seq
    val permute_profile: term permutation -> profile -> profile
    val pref_profileT: typ -> typ -> typ
    val preferred_alts: prefs -> term -> term list
    type prefs
    type profile
    val ranking: prefs -> term * term -> bool
    val relation_of_prefs: prefs -> (term * term) list
    val strict_pareto: profile -> term * term -> bool
    val strict_ranking: prefs -> term * term -> bool
    type support
  end
structure Preference_Profiles: PREFERENCE_PROFILES
locale election
  fixes agents :: "'agent set"
    and alts :: "'alt set"
  assumes "election agents alts"
locale vnm_utility
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and u :: "'a \<Rightarrow> real"
  assumes "vnm_utility carrier le u"
### theory "Randomised_Social_Choice.Utility_Functions"
### 1.364s elapsed time, 5.056s cpu time, 0.000s GC time
Loading theory "Randomised_Social_Choice.Stochastic_Dominance" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes")
locale preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "Order_Predicates.preorder_on carrier le"
signature PREFERENCE_PROFILES_CMD =
  sig
    val add_info: term -> info -> Context.generic -> Context.generic
    val get_info: term -> Proof.context -> info
    type info
    val preference_profile:
       (term * term) * (binding * (term * term list list) list) list ->
         Proof.context -> Proof.state
    val preference_profile_cmd:
       (string * string) * (binding * (string * string list list) list) list
         -> Proof.context -> Proof.state
    val transform_info: info -> morphism -> info
  end
structure Preference_Profiles_Cmd: PREFERENCE_PROFILES_CMD
### theory "Randomised_Social_Choice.Preference_Profile_Cmd"
### 1.563s elapsed time, 5.852s cpu time, 0.000s GC time
locale pref_profile_wf
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_wf agents alts R"
locale pref_profile_wf
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_wf agents alts R"
locale pref_profile_wf
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_wf agents alts R"
locale finite_total_preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "finite_total_preorder_on carrier le"
### theory "Randomised_Social_Choice.Stochastic_Dominance"
### 1.003s elapsed time, 3.804s cpu time, 0.476s GC time
Loading theory "Randomised_Social_Choice.SD_Efficiency" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes")
locale pref_profile_wf
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_wf agents alts R"
Found termination order: "size <*mlex*> {}"
### theory "Randomised_Social_Choice.SD_Efficiency"
### 0.652s elapsed time, 2.608s cpu time, 0.000s GC time
Loading theory "Randomised_Social_Choice.Social_Decision_Schemes" (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering")
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. length (snd p)) (fst p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. length (snd p)) (fst p)) <*mlex*> {}"
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
*** Failed to finish proof (line 462 of "$AFP/Randomised_Social_Choice/Stochastic_Dominance.thy"):
*** goal (1 subgoal):
***  1. \<lbrakk>sum (pmf p) (carrier \<inter> Collect (le x)) +
***              (\<Sum>a\<in>carrier.
***                 \<epsilon> *
***                 (pmf p a * real (length xs - weak_ranking_index a)))
***              \<le> sum (pmf q) (carrier \<inter> Collect (le x)) +
***                    (\<Sum>a\<in>carrier.
***                       \<epsilon> *
***                       (pmf q a * real (length xs - weak_ranking_index a)));
***      x \<in> carrier; {y. le x y} \<subseteq> carrier;
***      \<And>x y. le x y \<Longrightarrow> x \<in> carrier;
***      \<And>x y. le x y \<Longrightarrow> y \<in> 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")
### Ignoring duplicate rewrite rule:
### 0 \<le> pmf ?p1 ?x1 \<equiv> True
locale election
  fixes agents :: "'agent set"
    and alts :: "'alt set"
  assumes "election agents alts"
locale social_decision_scheme
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "social_decision_scheme agents alts sds"
locale anonymous_sds
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "anonymous_sds agents alts sds"
locale neutral_sds
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "neutral_sds agents alts sds"
locale an_sds
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "an_sds agents alts sds"
locale ex_post_efficient_sds
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "ex_post_efficient_sds agents alts sds"
locale sd_efficient_sds
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "sd_efficient_sds agents alts sds"
### Ignoring duplicate rewrite rule:
### mset (map ?f1 ?xs1) \<equiv> image_mset ?f1 (mset ?xs1)
locale social_decision_scheme
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "social_decision_scheme agents alts sds"
locale strategyproof_sds
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "strategyproof_sds agents alts sds"
locale social_decision_scheme
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "social_decision_scheme agents alts sds"
locale strongly_strategyproof_sds
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "strongly_strategyproof_sds agents alts sds"
locale strategyproof_an_sds
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
  assumes "strategyproof_an_sds agents alts sds"
### theory "Randomised_Social_Choice.Social_Decision_Schemes"
### 4.137s elapsed time, 14.428s cpu time, 0.368s GC time
Loading theory "Randomised_Social_Choice.SDS_Automation"
Loading theory "Randomised_Social_Choice.Random_Dictatorship" (required by "Randomised_Social_Choice.Randomised_Social_Choice")
Loading theory "Randomised_Social_Choice.SDS_Lowering" (required by "Randomised_Social_Choice.Randomised_Social_Choice")
locale election
  fixes agents :: "'agent set"
    and alts :: "'alt set"
  assumes "election agents alts"
### theory "Randomised_Social_Choice.Random_Dictatorship"
### 0.249s elapsed time, 0.892s cpu time, 0.000s GC time
Loading theory "Randomised_Social_Choice.Random_Serial_Dictatorship" (required by "Randomised_Social_Choice.Randomised_Social_Choice")
locale sds_lowering
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
    and agents' :: "'agent set"
    and alts' :: "'alt set"
  assumes "sds_lowering agents alts sds agents' alts'"
locale pref_profile_wf
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    R :: "'agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool"
  assumes "pref_profile_wf agents alts R"
locale sds_lowering_anonymous
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
    and agents' :: "'agent set"
    and alts' :: "'alt set"
  assumes "sds_lowering_anonymous agents alts sds agents' alts'"
locale election
  fixes agents :: "'agent set"
    and alts :: "'alt set"
  assumes "election agents alts"
locale sds_lowering_neutral
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
    and agents' :: "'agent set"
    and alts' :: "'alt set"
  assumes "sds_lowering_neutral agents alts sds agents' alts'"
### theory "Randomised_Social_Choice.Random_Serial_Dictatorship"
### 0.643s elapsed time, 2.564s cpu time, 0.000s GC time
locale sds_lowering_sd_efficient
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
    and agents' :: "'agent set"
    and alts' :: "'alt set"
  assumes "sds_lowering_sd_efficient agents alts sds agents' alts'"
locale sds_lowering_strategyproof
  fixes agents :: "'agent set"
    and alts :: "'alt set"
    and
    sds ::
      "('agent \<Rightarrow> 'alt \<Rightarrow> 'alt \<Rightarrow> bool)
       \<Rightarrow> 'alt pmf"
    and agents' :: "'agent set"
    and alts' :: "'alt set"
  assumes "sds_lowering_strategyproof agents alts sds agents' alts'"
locale sds_lowering_anonymous_neutral_sdeff_stratproof
  fixes agents :: "'a set"
    and alts :: "'b set"
    and
    sds ::
      "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> bool)
       \<Rightarrow> 'b pmf"
    and agents' :: "'a set"
    and alts' :: "'b set"
  assumes
    "sds_lowering_anonymous_neutral_sdeff_stratproof agents alts sds agents'
      alts'"
### theory "Randomised_Social_Choice.SDS_Lowering"
### 1.097s elapsed time, 4.280s cpu time, 0.000s GC time
Loading theory "Randomised_Social_Choice.Randomised_Social_Choice"
### theory "Randomised_Social_Choice.Randomised_Social_Choice"
### 0.466s elapsed time, 1.864s cpu time, 0.000s GC time
### Ignoring duplicate rewrite rule:
### 0 \<le> Sigma_Algebra.measure ?M1 ?A1 \<equiv> True
consts
  pref_classes_lists :: "'a set list \<Rightarrow> 'a set set"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
locale preorder_on
  fixes carrier :: "'a set"
    and le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  assumes "Order_Predicates.preorder_on carrier le"
signature RANDOMISED_SOCIAL_CHOICE =
  sig
    val find_inefficiency_witness:
       Preference_Profiles.profile ->
         Preference_Profiles.support -> (lottery * term) option
    val find_minimal_inefficient_supports:
       Preference_Profiles.profile ->
         (Preference_Profiles.support * lottery * term) list
    type lottery
    val lotteryT: typ -> typ
    val mk_inefficiency_lp:
       Preference_Profiles.profile ->
         Preference_Profiles.support -> (string list * string * int) list
    val mk_support_witness:
       Preference_Profiles.profile ->
         Preference_Profiles.support * lottery ->
           Preference_Profiles.support * lottery * term
    val probability: lottery -> term list -> Rat.rat
    val sdsT: typ -> typ -> typ
    val stochastic_dominance:
       Preference_Profiles.prefs -> lottery * lottery -> bool
    val strict_stochastic_dominance:
       Preference_Profiles.prefs -> lottery * lottery -> bool
  end
structure Randomised_Social_Choice: RANDOMISED_SOCIAL_CHOICE
### ML warning (line 104 of "$AFP/Randomised_Social_Choice/Automation/sds_automation.ML"):
### Pattern is not exhaustive.
### ML warning (line 126 of "$AFP/Randomised_Social_Choice/Automation/sds_automation.ML"):
### Pattern is not exhaustive.
### ML warning (line 133 of "$AFP/Randomised_Social_Choice/Automation/sds_automation.ML"):
### Pattern is not exhaustive.
### ML warning (line 121 of "$AFP/Randomised_Social_Choice/Automation/sds_automation.ML"):
### Value identifier (sds) has not been referenced.
### ML warning (line 248 of "$AFP/Randomised_Social_Choice/Automation/sds_automation.ML"):
### Pattern is not exhaustive.
### ML warning (line 492 of "$AFP/Randomised_Social_Choice/Automation/sds_automation.ML"):
### Pattern is not exhaustive.
### ML warning (line 499 of "$AFP/Randomised_Social_Choice/Automation/sds_automation.ML"):
### Pattern is not exhaustive.
### ML warning (line 487 of "$AFP/Randomised_Social_Choice/Automation/sds_automation.ML"):
### Value identifier (sds) has not been referenced.
val prove_in_set = fn: Proof.context -> term -> thm
val prove_in_list = fn: Proof.context -> term -> term list -> thm
val eval_inverse_permutation_of_list_conv = fn:
   thm -> Proof.context -> cterm -> thm
val dest_wf_thm = fn: thm -> term
val gen_derive_orbit_equations = fn:
   Proof.context -> thm option -> term list -> Proof.state
val derive_orbit_equations_cmd = fn:
   thm option -> string list -> Proof.context -> Proof.state
val optional_thm_parser = fn:
   Token.T list -> (Facts.ref * Token.src list) option * Token.T list
val optional_thms_parser = fn:
   Token.T list -> (Facts.ref * Token.src list) list option * Token.T list
val gen_prepare_ex_post_conditions = fn:
   ((term * term list list) list -> (term * term * term) list) ->
     term -> Preference_Profiles_Cmd.info -> Proof.context -> thm list
val prepare_find_ex_post_conditions = fn:
   term -> Preference_Profiles_Cmd.info -> Proof.context -> thm list
val prepare_ex_post_conditions = fn:
   (Preference_Profiles.profile * term) list ->
     term -> Preference_Profiles_Cmd.info -> Proof.context -> thm list
val gen_prepare_sdeff_conditions = fn:
   ((term * term list list) list ->
      (term list * (term * Rat.rat) list * term) list)
     -> term -> Preference_Profiles_Cmd.info -> Proof.context -> thm list
val prepare_find_sdeff_conditions = fn:
   term -> Preference_Profiles_Cmd.info -> Proof.context -> thm list
val prepare_sdeff_conditions_from_wits = fn:
   (Preference_Profiles.profile * Preference_Profiles.support *
    Randomised_Social_Choice.lottery option
   )
   list
     -> term -> Preference_Profiles_Cmd.info -> Proof.context -> thm list
val gen_derive_support_conditions = fn:
   (term -> Preference_Profiles_Cmd.info -> Proof.context -> thm list) list
     -> thm list option -> term list -> Proof.context -> Proof.state
val gen_derive_support_conditions_cmd = fn:
   (term -> Preference_Profiles_Cmd.info -> Proof.context -> thm list) list
     -> thm list option -> string list -> Proof.context -> Proof.state
val derive_support_conditions_cmd = fn:
   thm list option -> string list -> Proof.context -> Proof.state
val derive_ex_post_conditions_cmd = fn:
   thm list option -> string list -> Proof.context -> Proof.state
val find_inefficient_supports = fn:
   Preference_Profiles.profile ->
     (term list * Randomised_Social_Choice.lottery option) list
val find_sd_inefficient_supports_cmd = fn:
   string list -> Proof.context -> unit
val prove_sd_inefficient_supports_cmd = fn:
   thm list option ->
     ((string * string list) * (string * Rat.rat) list option) list ->
       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"
### 4.365s elapsed time, 16.796s cpu time, 0.752s GC time
### Ignoring duplicate rewrite rule:
### mset (map ?f1 ?xs1) \<equiv> image_mset ?f1 (mset ?xs1)
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 462 of "$AFP/Randomised_Social_Choice/Stochastic_Dominance.thy"):
*** goal (1 subgoal):
***  1. \<lbrakk>sum (pmf p) (carrier \<inter> Collect (le x)) +
***              (\<Sum>a\<in>carrier.
***                 \<epsilon> *
***                 (pmf p a * real (length xs - weak_ranking_index a)))
***              \<le> sum (pmf q) (carrier \<inter> Collect (le x)) +
***                    (\<Sum>a\<in>carrier.
***                       \<epsilon> *
***                       (pmf q a * real (length xs - weak_ranking_index a)));
***      x \<in> carrier; {y. le x y} \<subseteq> carrier;
***      \<And>x y. le x y \<Longrightarrow> x \<in> carrier;
***      \<And>x y. le x y \<Longrightarrow> y \<in> 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")