[STATEMENT]
lemma Dom_assume:
  "Dom([b]\<^sup>\<top>) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom ?[b] = b
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma Dom_seq:
  "Dom(P ;; Q) = Dom(P ;; [Dom(Q)]\<^sup>\<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom (P ;; Q) = Dom (P ;; ?[Dom Q])
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma Dom_disj:
  "Dom(P \<or> Q) = (Dom(P) \<or> Dom(Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom (P \<or> Q) = (Dom P \<or> Dom Q)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma Dom_inf:
  "Dom(P \<sqinter> Q) = (Dom(P) \<or> Dom(Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom (P \<sqinter> Q) = (Dom P \<or> Dom Q)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma assume_Dom:
  "[Dom(P)]\<^sup>\<top> ;; P = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ?[Dom P] ;; P = P
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma base_pref_is_ord_eucl_rpr: "i \<in> agents \<Longrightarrow> rational_preference consumption_set Pr[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> agents \<Longrightarrow> rational_preference consumption_set Pr[i]
[PROOF STEP]
by (meson exchange_economy.agent_props exchange_economy_axioms
      ord_eucl_utility_imp_rpr real_vector_rpr.have_rpr)


[STATEMENT]
lemma utility_function_def[iff]:
  assumes "i \<in> agents"
  shows "U[i] x \<ge> U[i] y \<longleftrightarrow> x \<succeq>[Pr[i]] y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (U[i] y \<le> U[i] x) = x \<succeq>[Pr[i]] y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. U[i] y \<le> U[i] x \<Longrightarrow> x \<succeq>[Pr[i]] y
 2. x \<succeq>[Pr[i]] y \<Longrightarrow> U[i] y \<le> U[i] x
[PROOF STEP]
have "ordinal_utility consumption_set (Pref i) (U[i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_utility consumption_set Pr[i] U[i]
[PROOF STEP]
using agent_props assms eucl_ordinal_utility_def
[PROOF STATE]
proof (prove)
using this:
?i \<in> agents \<Longrightarrow> eucl_ordinal_utility consumption_set Pr[?i] U[?i]
i \<in> agents
eucl_ordinal_utility ?carrier ?relation ?u \<equiv> ordinal_utility ?carrier ?relation ?u

goal (1 subgoal):
 1. ordinal_utility consumption_set Pr[i] U[i]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ordinal_utility consumption_set Pr[i] U[i]

goal (2 subgoals):
 1. U[i] y \<le> U[i] x \<Longrightarrow> x \<succeq>[Pr[i]] y
 2. x \<succeq>[Pr[i]] y \<Longrightarrow> U[i] y \<le> U[i] x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ordinal_utility consumption_set Pr[i] U[i]
[PROOF STEP]
show " U[i] y \<le>  U[i] x \<Longrightarrow> x \<succeq>[Pref i] y"
[PROOF STATE]
proof (prove)
using this:
ordinal_utility consumption_set Pr[i] U[i]

goal (1 subgoal):
 1. U[i] y \<le> U[i] x \<Longrightarrow> x \<succeq>[Pr[i]] y
[PROOF STEP]
by (meson UNIV_I cons_set_props ordinal_utility.util_def_conf
        pre_arrow_debreu_consumption_set_def)
[PROOF STATE]
proof (state)
this:
U[i] y \<le> U[i] x \<Longrightarrow> x \<succeq>[Pr[i]] y

goal (1 subgoal):
 1. x \<succeq>[Pr[i]] y \<Longrightarrow> U[i] y \<le> U[i] x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<succeq>[Pr[i]] y \<Longrightarrow> U[i] y \<le> U[i] x
[PROOF STEP]
show "x \<succeq>[Pref i] y \<Longrightarrow> U[i] y \<le> U[i] x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<succeq>[Pr[i]] y \<Longrightarrow> U[i] y \<le> U[i] x
[PROOF STEP]
by (meson agent_props assms ordinal_utility_def eucl_ordinal_utility_def)
[PROOF STATE]
proof (state)
this:
x \<succeq>[Pr[i]] y \<Longrightarrow> U[i] y \<le> U[i] x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma budget_constraint_is_feasible:
  assumes "i \<in> agents"
  assumes "X \<in> (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
  shows "P \<bullet> X \<le> P \<bullet> \<E>[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> X \<le> P \<bullet> \<E>[i]
[PROOF STEP]
using budget_constraint_def assms
[PROOF STATE]
proof (prove)
using this:
budget_constraint ?f ?S ?W = {x \<in> ?S. ?f x \<le> ?W}
i \<in> agents
X \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. P \<bullet> X \<le> P \<bullet> \<E>[i]
[PROOF STEP]
by (simp add: budget_constraint_def)


[STATEMENT]
lemma arg_max_set_therefore_no_better :
  assumes "i \<in> agents"
  assumes "x \<in> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
  shows "U[i] y > U[i] x \<longrightarrow> y \<notin> budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U[i] x < U[i] y \<longrightarrow> y \<notin> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
by (meson no_better_in_s assms)


[STATEMENT]
lemma consumption_set_member: "\<forall>x. x \<in> consumption_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> consumption_set
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. x \<in> consumption_set
[PROOF STEP]
have "\<And>(x::'a). x \<in> consumption_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> consumption_set
[PROOF STEP]
using cons_set_props pre_arrow_debreu_consumption_set_def
[PROOF STATE]
proof (prove)
using this:
pre_arrow_debreu_consumption_set consumption_set
pre_arrow_debreu_consumption_set ?consumption_set \<equiv> \<forall>x. x \<in> UNIV \<longrightarrow> x \<in> ?consumption_set

goal (1 subgoal):
 1. \<And>x. x \<in> consumption_set
[PROOF STEP]
by (simp add: pre_arrow_debreu_consumption_set_def)
[PROOF STATE]
proof (state)
this:
?x1 \<in> consumption_set

goal (1 subgoal):
 1. \<forall>x. x \<in> consumption_set
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> consumption_set

goal (1 subgoal):
 1. \<forall>x. x \<in> consumption_set
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> consumption_set

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma argmax_entire_budget :
  assumes "i \<in> agents"
  assumes "local_nonsatiation consumption_set Pr[i]"
  assumes "X \<in> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
  shows "P \<bullet> X = P \<bullet> \<E>[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> X = P \<bullet> \<E>[i]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<bullet> X = P \<bullet> \<E>[i]
[PROOF STEP]
have leq : "(P \<bullet> X) \<le> (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> X \<le> P \<bullet> \<E>[i]
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<bullet> X \<le> P \<bullet> \<E>[i]
[PROOF STEP]
have "X \<in> budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
using argmax_sol_in_s[of X "U[i]" "budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"]
        assms
[PROOF STATE]
proof (prove)
using this:
X \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])) \<Longrightarrow> X \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
i \<in> agents
local_nonsatiation consumption_set Pr[i]
X \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))

goal (1 subgoal):
 1. X \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. P \<bullet> X \<le> P \<bullet> \<E>[i]
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
X \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. P \<bullet> X \<le> P \<bullet> \<E>[i]
[PROOF STEP]
using assms(1) budget_constraint_is_feasible
[PROOF STATE]
proof (prove)
using this:
X \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
i \<in> agents
\<lbrakk>?i \<in> agents; ?X \<in> budget_constraint ((\<bullet>) ?P) consumption_set (?P \<bullet> \<E>[?i])\<rbrakk> \<Longrightarrow> ?P \<bullet> ?X \<le> ?P \<bullet> \<E>[?i]

goal (1 subgoal):
 1. P \<bullet> X \<le> P \<bullet> \<E>[i]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<bullet> X \<le> P \<bullet> \<E>[i]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<bullet> X \<le> P \<bullet> \<E>[i]

goal (1 subgoal):
 1. P \<bullet> X = P \<bullet> \<E>[i]
[PROOF STEP]
have not_less: "\<not>(P \<bullet> X < P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P \<bullet> X < P \<bullet> \<E>[i]
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<bullet> X < P \<bullet> \<E>[i] \<Longrightarrow> False
[PROOF STEP]
assume cpos: "(P \<bullet> X) < (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (state)
this:
P \<bullet> X < P \<bullet> \<E>[i]

goal (1 subgoal):
 1. P \<bullet> X < P \<bullet> \<E>[i] \<Longrightarrow> False
[PROOF STEP]
define lesS where "lesS = {x. P \<bullet> x < P \<bullet> \<E>[i]}"
[PROOF STATE]
proof (state)
this:
lesS = {x. P \<bullet> x < P \<bullet> \<E>[i]}

goal (1 subgoal):
 1. P \<bullet> X < P \<bullet> \<E>[i] \<Longrightarrow> False
[PROOF STEP]
obtain e where
      e: "0 < e" "ball X e \<subseteq> lesS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; ball X e \<subseteq> lesS\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis cpos lesS_def mem_Collect_eq
          open_contains_ball_eq open_halfspace_lt)
[PROOF STATE]
proof (state)
this:
0 < e
ball X e \<subseteq> lesS

goal (1 subgoal):
 1. P \<bullet> X < P \<bullet> \<E>[i] \<Longrightarrow> False
[PROOF STEP]
obtain Y where
      Y: "Y \<succ>[Pref i] X " "Y \<in> ball X e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>Y \<succeq>[Pr[i]] X \<and> (X, Y) \<notin> Pr[i]; Y \<in> ball X e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using e consumption_set_member assms
[PROOF STATE]
proof (prove)
using this:
0 < e
ball X e \<subseteq> lesS
\<forall>x. x \<in> consumption_set
i \<in> agents
local_nonsatiation consumption_set Pr[i]
X \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>Y \<succeq>[Pr[i]] X \<and> (X, Y) \<notin> Pr[i]; Y \<in> ball X e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y \<succeq>[Pr[i]] X \<and> (X, Y) \<notin> Pr[i]
Y \<in> ball X e

goal (1 subgoal):
 1. P \<bullet> X < P \<bullet> \<E>[i] \<Longrightarrow> False
[PROOF STEP]
have "Y \<in> consumption_set"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y \<in> consumption_set
[PROOF STEP]
using consumption_set_member
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> consumption_set

goal (1 subgoal):
 1. Y \<in> consumption_set
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Y \<in> consumption_set

goal (1 subgoal):
 1. P \<bullet> X < P \<bullet> \<E>[i] \<Longrightarrow> False
[PROOF STEP]
hence "Y \<in> budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
using this:
Y \<in> consumption_set

goal (1 subgoal):
 1. Y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
using budget_constraint_def e lesS_def
        less_eq_real_def Y
[PROOF STATE]
proof (prove)
using this:
Y \<in> consumption_set
budget_constraint ?f ?S ?W = {x \<in> ?S. ?f x \<le> ?W}
0 < e
ball X e \<subseteq> lesS
lesS = {x. P \<bullet> x < P \<bullet> \<E>[i]}
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
Y \<succeq>[Pr[i]] X \<and> (X, Y) \<notin> Pr[i]
Y \<in> ball X e

goal (1 subgoal):
 1. Y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. P \<bullet> X < P \<bullet> \<E>[i] \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
Y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. False
[PROOF STEP]
by (meson assms Y all_leq utility_function_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> P \<bullet> X < P \<bullet> \<E>[i]

goal (1 subgoal):
 1. P \<bullet> X = P \<bullet> \<E>[i]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> X = P \<bullet> \<E>[i]
[PROOF STEP]
using leq not_less
[PROOF STATE]
proof (prove)
using this:
P \<bullet> X \<le> P \<bullet> \<E>[i]
\<not> P \<bullet> X < P \<bullet> \<E>[i]

goal (1 subgoal):
 1. P \<bullet> X = P \<bullet> \<E>[i]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<bullet> X = P \<bullet> \<E>[i]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pref_more_expensive:
  assumes "i \<in> agents"
  assumes "x \<in> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
  assumes "U[i] y > U[i] x"
  shows "y \<bullet> P > P \<bullet> \<E>[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> \<E>[i] < y \<bullet> P
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P \<bullet> \<E>[i] < y \<bullet> P \<Longrightarrow> False
[PROOF STEP]
assume cpos :  "\<not>(y \<bullet> P > P \<bullet> \<E>[i])"
[PROOF STATE]
proof (state)
this:
\<not> P \<bullet> \<E>[i] < y \<bullet> P

goal (1 subgoal):
 1. \<not> P \<bullet> \<E>[i] < y \<bullet> P \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> P \<bullet> \<E>[i] < y \<bullet> P
[PROOF STEP]
have xp_leq : "y \<bullet> P \<le> P \<bullet>  \<E>[i]"
[PROOF STATE]
proof (prove)
using this:
\<not> P \<bullet> \<E>[i] < y \<bullet> P

goal (1 subgoal):
 1. y \<bullet> P \<le> P \<bullet> \<E>[i]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<bullet> P \<le> P \<bullet> \<E>[i]

goal (1 subgoal):
 1. \<not> P \<bullet> \<E>[i] < y \<bullet> P \<Longrightarrow> False
[PROOF STEP]
hence "x \<in> budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
using this:
y \<bullet> P \<le> P \<bullet> \<E>[i]

goal (1 subgoal):
 1. x \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
using argmax_sol_in_s[of x " U[i]" "budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"]
      assms
[PROOF STATE]
proof (prove)
using this:
y \<bullet> P \<le> P \<bullet> \<E>[i]
x \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])) \<Longrightarrow> x \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
i \<in> agents
x \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))
U[i] x < U[i] y

goal (1 subgoal):
 1. x \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. \<not> P \<bullet> \<E>[i] < y \<bullet> P \<Longrightarrow> False
[PROOF STEP]
hence xp_in: "y \<in> budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
using this:
x \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]) \<Longrightarrow> y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
have "P \<bullet> y \<le> P \<bullet> \<E>[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> y \<le> P \<bullet> \<E>[i]
[PROOF STEP]
by (metis xp_leq inner_commute)
[PROOF STATE]
proof (state)
this:
P \<bullet> y \<le> P \<bullet> \<E>[i]

goal (1 subgoal):
 1. x \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]) \<Longrightarrow> y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<bullet> y \<le> P \<bullet> \<E>[i]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<bullet> y \<le> P \<bullet> \<E>[i]

goal (1 subgoal):
 1. y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
using consumption_set_member
[PROOF STATE]
proof (prove)
using this:
P \<bullet> y \<le> P \<bullet> \<E>[i]
\<forall>x. x \<in> consumption_set

goal (1 subgoal):
 1. y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
by (simp add: budget_constraint_def)
[PROOF STATE]
proof (state)
this:
y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. \<not> P \<bullet> \<E>[i] < y \<bullet> P \<Longrightarrow> False
[PROOF STEP]
hence "y \<succ>[Pref i] x"
[PROOF STATE]
proof (prove)
using this:
y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]
[PROOF STEP]
using arg_max_set_therefore_no_better assms
[PROOF STATE]
proof (prove)
using this:
y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
\<lbrakk>?i \<in> agents; ?x \<in> arg_max_set U[?i] (budget_constraint ((\<bullet>) ?P) consumption_set (?P \<bullet> \<E>[?i]))\<rbrakk> \<Longrightarrow> U[?i] ?x < U[?i] ?y \<longrightarrow> ?y \<notin> budget_constraint ((\<bullet>) ?P) consumption_set (?P \<bullet> \<E>[?i])
i \<in> agents
x \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))
U[i] x < U[i] y

goal (1 subgoal):
 1. y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]

goal (1 subgoal):
 1. \<not> P \<bullet> \<E>[i] < y \<bullet> P \<Longrightarrow> False
[PROOF STEP]
hence "y \<succ>[Pref i] x \<and> y \<in> budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
using this:
y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]

goal (1 subgoal):
 1. (y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]) \<and> y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
using xp_in
[PROOF STATE]
proof (prove)
using this:
y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]
y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. (y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]) \<and> y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]) \<and> y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. \<not> P \<bullet> \<E>[i] < y \<bullet> P \<Longrightarrow> False
[PROOF STEP]
hence "x \<notin> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
[PROOF STATE]
proof (prove)
using this:
(y \<succeq>[Pr[i]] x \<and> (x, y) \<notin> Pr[i]) \<and> y \<in> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. x \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))
[PROOF STEP]
by (meson assms exchange_economy.arg_max_set_therefore_no_better
        exchange_economy_axioms)
[PROOF STATE]
proof (state)
this:
x \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))

goal (1 subgoal):
 1. \<not> P \<bullet> \<E>[i] < y \<bullet> P \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
x \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))
x \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma same_util_is_equal_or_more_expensive:
  assumes "i \<in> agents"
  assumes "local_nonsatiation consumption_set Pr[i]"
  assumes "x \<in> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
  assumes "U[i] y \<ge> U[i] x"
  shows "y \<bullet> P \<ge> P \<bullet> \<E>[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> \<E>[i] \<le> y \<bullet> P
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<bullet> \<E>[i] \<le> y \<bullet> P
[PROOF STEP]
have not_in: "y \<notin> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))
    \<Longrightarrow> y \<bullet> P > P \<bullet> \<E>[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])) \<Longrightarrow> P \<bullet> \<E>[i] < y \<bullet> P
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])) \<Longrightarrow> P \<bullet> \<E>[i] < y \<bullet> P
[PROOF STEP]
assume "y \<notin> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
[PROOF STATE]
proof (state)
this:
y \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))

goal (1 subgoal):
 1. y \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])) \<Longrightarrow> P \<bullet> \<E>[i] < y \<bullet> P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))
[PROOF STEP]
have "y \<notin> budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i])"
[PROOF STATE]
proof (prove)
using this:
y \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))

goal (1 subgoal):
 1. y \<notin> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
by (meson assms leq_all_in_sol assms)
[PROOF STATE]
proof (state)
this:
y \<notin> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. y \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])) \<Longrightarrow> P \<bullet> \<E>[i] < y \<bullet> P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<notin> budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])

goal (1 subgoal):
 1. P \<bullet> \<E>[i] < y \<bullet> P
[PROOF STEP]
by (simp add: budget_constraint_def inner_commute
          consumption_set_member)
[PROOF STATE]
proof (state)
this:
P \<bullet> \<E>[i] < y \<bullet> P

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<notin> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i])) \<Longrightarrow> P \<bullet> \<E>[i] < y \<bullet> P

goal (1 subgoal):
 1. P \<bullet> \<E>[i] \<le> y \<bullet> P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> \<E>[i] \<le> y \<bullet> P
[PROOF STEP]
by (metis argmax_entire_budget not_in assms(1,2,3)
        dual_order.order_iff_strict inner_commute)
[PROOF STATE]
proof (state)
this:
P \<bullet> \<E>[i] \<le> y \<bullet> P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_in_argmax_same_price:
  assumes "i \<in> agents"
  assumes "local_nonsatiation consumption_set Pr[i]"
  assumes "x \<in> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
    and  "y \<in> arg_max_set U[i] (budget_constraint (calculate_value P) consumption_set (P \<bullet> \<E>[i]))"
  shows "P \<bullet> x = P \<bullet> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<bullet> x = P \<bullet> y
[PROOF STEP]
using argmax_entire_budget assms(1) assms(2) assms(3) assms(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<in> agents; local_nonsatiation consumption_set Pr[?i]; ?X \<in> arg_max_set U[?i] (budget_constraint ((\<bullet>) ?P) consumption_set (?P \<bullet> \<E>[?i]))\<rbrakk> \<Longrightarrow> ?P \<bullet> ?X = ?P \<bullet> \<E>[?i]
i \<in> agents
local_nonsatiation consumption_set Pr[i]
x \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))
y \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) P) consumption_set (P \<bullet> \<E>[i]))

goal (1 subgoal):
 1. P \<bullet> x = P \<bullet> y
[PROOF STEP]
by presburger


[STATEMENT]
lemma individual_rationalism :
  assumes "comp_equilib_endow P X \<E>"
  shows "\<forall>i \<in> agents. X i \<succeq>[Pref i] \<E>[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>agents. X i \<succeq>[Pr[i]] \<E>[i]
[PROOF STEP]
by (metis pref_more_expensive comp_equilib_endow_def assms
      inner_commute less_irrefl not_le utility_function_def)


[STATEMENT]
lemma walras_law_per_agent :
  assumes "\<And>i. i \<in> agents \<Longrightarrow> local_nonsatiation consumption_set Pr[i]"
  assumes "comp_equilib_endow P X \<E>"
  shows "\<forall>i \<in> agents. P \<bullet> X i = P \<bullet> \<E>[i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>agents. P \<bullet> X i = P \<bullet> \<E>[i]
[PROOF STEP]
by (meson argmax_entire_budget comp_equilib_endow_def assms)


[STATEMENT]
lemma walras_law:
  assumes "\<And>i. i \<in> agents \<Longrightarrow> local_nonsatiation consumption_set Pr[i]"
  assumes "comp_equilib_endow P X \<E>"
  shows "(\<Sum>i\<in>agents. P \<bullet> (X i)) - (\<Sum>i\<in>agents. P \<bullet> \<E>[i]) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>agents. P \<bullet> X i) - (\<Sum>i\<in>agents. P \<bullet> \<E>[i]) = 0
[PROOF STEP]
using assms walras_law_per_agent
[PROOF STATE]
proof (prove)
using this:
?i1 \<in> agents \<Longrightarrow> local_nonsatiation consumption_set Pr[?i1]
comp_equilib_endow P X \<E>
\<lbrakk>\<And>i. i \<in> agents \<Longrightarrow> local_nonsatiation consumption_set Pr[i]; comp_equilib_endow ?P ?X \<E>\<rbrakk> \<Longrightarrow> \<forall>i\<in>agents. ?P \<bullet> ?X i = ?P \<bullet> \<E>[i]

goal (1 subgoal):
 1. (\<Sum>i\<in>agents. P \<bullet> X i) - (\<Sum>i\<in>agents. P \<bullet> \<E>[i]) = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma inner_with_ge_0: "(P::(real, 'n::finite) vec) > 0 \<Longrightarrow> A \<ge> B \<Longrightarrow>  P \<bullet> A \<ge> P \<bullet> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < P; B \<le> A\<rbrakk> \<Longrightarrow> P \<bullet> B \<le> P \<bullet> A
[PROOF STEP]
by (metis dual_order.order_iff_strict inner_commute
      interval_inner_leI(2) ord_class.atLeastAtMost_iff)


[STATEMENT]
theorem first_welfare_theorem_exchange:
  assumes lns : "\<And>i. i \<in> agents \<Longrightarrow> local_nonsatiation consumption_set Pr[i]"
    and price_cond: "Price > 0"
  assumes equilibrium : "comp_equilib_endow Price \<X> \<E>"
  shows "pareto_optimal_endow \<X> \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pareto_optimal_endow \<X> \<E>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
assume neg_ass : "\<not> pareto_optimal_endow \<X> \<E>"
[PROOF STATE]
proof (state)
this:
\<not> pareto_optimal_endow \<X> \<E>

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
have equili_feasible : "feasible_allocation \<X> \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. feasible_allocation \<X> \<E>
[PROOF STEP]
using comp_equilib_endow_def equilibrium
[PROOF STATE]
proof (prove)
using this:
comp_equilib_endow ?P ?X ?E \<equiv> feasible_allocation ?X ?E \<and> (\<forall>i\<in>agents. ?X i \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) ?P) consumption_set (?P \<bullet> ?E i)))
comp_equilib_endow Price \<X> \<E>

goal (1 subgoal):
 1. feasible_allocation \<X> \<E>
[PROOF STEP]
by (simp add: comp_equilib_endow_def)
[PROOF STATE]
proof (state)
this:
feasible_allocation \<X> \<E>

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
have price_g_zero : "Price > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < Price
[PROOF STEP]
by (simp add: price_cond)
[PROOF STATE]
proof (state)
this:
(0::'a) < Price

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
obtain Y where
    xprime_pareto: "feasible_allocation Y \<E> \<and>
            (\<forall>i \<in> agents. U[i] (Y i) \<ge> U[i] (\<X> i)) \<and>
            (\<exists>i \<in> agents. U[i] (Y i) > U[i] (\<X> i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Y. feasible_allocation Y \<E> \<and> (\<forall>i\<in>agents. U[i] (\<X> i) \<le> U[i] (Y i)) \<and> (\<exists>i\<in>agents. U[i] (\<X> i) < U[i] (Y i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using equili_feasible neg_ass pareto_dominating_def
      pareto_optimal_endow_def
[PROOF STATE]
proof (prove)
using this:
feasible_allocation \<X> \<E>
\<not> pareto_optimal_endow \<X> \<E>
?X \<succ>Pareto ?Y = ((\<forall>i\<in>agents. U[i] (?Y i) \<le> U[i] (?X i)) \<and> (\<exists>i\<in>agents. U[i] (?Y i) < U[i] (?X i)))
pareto_optimal_endow ?X ?E = (feasible_allocation ?X ?E \<and> (\<nexists>X'. feasible_allocation X' ?E \<and> X' \<succ>Pareto ?X))

goal (1 subgoal):
 1. (\<And>Y. feasible_allocation Y \<E> \<and> (\<forall>i\<in>agents. U[i] (\<X> i) \<le> U[i] (Y i)) \<and> (\<exists>i\<in>agents. U[i] (\<X> i) < U[i] (Y i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
feasible_allocation Y \<E> \<and> (\<forall>i\<in>agents. U[i] (\<X> i) \<le> U[i] (Y i)) \<and> (\<exists>i\<in>agents. U[i] (\<X> i) < U[i] (Y i))

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
have is_feasible : "feasible_allocation Y \<E>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. feasible_allocation Y \<E>
[PROOF STEP]
using xprime_pareto
[PROOF STATE]
proof (prove)
using this:
feasible_allocation Y \<E> \<and> (\<forall>i\<in>agents. U[i] (\<X> i) \<le> U[i] (Y i)) \<and> (\<exists>i\<in>agents. U[i] (\<X> i) < U[i] (Y i))

goal (1 subgoal):
 1. feasible_allocation Y \<E>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
feasible_allocation Y \<E>

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
have all_great_eq_value : "\<forall>i \<in> agents. Price \<bullet> (Y i) \<ge> Price \<bullet> (\<X> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>agents. Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> agents \<Longrightarrow> Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> agents \<Longrightarrow> Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
assume "i \<in> agents"
[PROOF STATE]
proof (state)
this:
i \<in> agents

goal (1 subgoal):
 1. \<And>i. i \<in> agents \<Longrightarrow> Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
show "Price \<bullet> (Y i) \<ge> Price \<bullet> (\<X> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
have x_in_agmx : "(\<X> i) \<in> arg_max_set U[i] (budget_constraint (calculate_value Price) consumption_set (Price \<bullet> \<E>[i]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<X> i \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) Price) consumption_set (Price \<bullet> \<E>[i]))
[PROOF STEP]
by (meson \<open>i \<in> agents\<close> comp_equilib_endow_def equilibrium)
[PROOF STATE]
proof (state)
this:
\<X> i \<in> arg_max_set U[i] (budget_constraint ((\<bullet>) Price) consumption_set (Price \<bullet> \<E>[i]))

goal (1 subgoal):
 1. Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
have "( U[i]) (\<X> i) - U[i] (Y i) \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U[i] (\<X> i) - U[i] (Y i) \<le> 0
[PROOF STEP]
using \<open>i \<in> agents\<close> xprime_pareto
[PROOF STATE]
proof (prove)
using this:
i \<in> agents
feasible_allocation Y \<E> \<and> (\<forall>i\<in>agents. U[i] (\<X> i) \<le> U[i] (Y i)) \<and> (\<exists>i\<in>agents. U[i] (\<X> i) < U[i] (Y i))

goal (1 subgoal):
 1. U[i] (\<X> i) - U[i] (Y i) \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U[i] (\<X> i) - U[i] (Y i) \<le> 0

goal (1 subgoal):
 1. Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
hence "Price \<bullet> (\<X> i) - Price \<bullet> (Y i) \<le> 0"
[PROOF STATE]
proof (prove)
using this:
U[i] (\<X> i) - U[i] (Y i) \<le> 0

goal (1 subgoal):
 1. Price \<bullet> \<X> i - Price \<bullet> Y i \<le> 0
[PROOF STEP]
by (metis \<open>i \<in> agents\<close> argmax_entire_budget diff_le_0_iff_le x_in_agmx
            inner_commute lns same_util_is_equal_or_more_expensive)
[PROOF STATE]
proof (state)
this:
Price \<bullet> \<X> i - Price \<bullet> Y i \<le> 0

goal (1 subgoal):
 1. Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Price \<bullet> \<X> i - Price \<bullet> Y i \<le> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Price \<bullet> \<X> i - Price \<bullet> Y i \<le> 0

goal (1 subgoal):
 1. Price \<bullet> \<X> i \<le> Price \<bullet> Y i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Price \<bullet> \<X> i \<le> Price \<bullet> Y i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Price \<bullet> \<X> i \<le> Price \<bullet> Y i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>agents. Price \<bullet> \<X> i \<le> Price \<bullet> Y i

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
have ex_greater_value : "\<exists>i \<in> agents. Price \<bullet> (Y i) > Price \<bullet> (\<X> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i\<in>agents. Price \<bullet> \<X> i < Price \<bullet> Y i
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>i\<in>agents. Price \<bullet> \<X> i < Price \<bullet> Y i) \<Longrightarrow> False
[PROOF STEP]
assume a1 : "\<not>(\<exists>i \<in> agents. Price \<bullet> (Y i) > Price \<bullet> (\<X> i))"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>i\<in>agents. Price \<bullet> \<X> i < Price \<bullet> Y i)

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>agents. Price \<bullet> \<X> i < Price \<bullet> Y i) \<Longrightarrow> False
[PROOF STEP]
obtain i where
      obt_witness : "i \<in> agents" "U[i] (Y i) > ( U[i]) (\<X> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> agents; U[i] (\<X> i) < U[i] (Y i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xprime_pareto
[PROOF STATE]
proof (prove)
using this:
feasible_allocation Y \<E> \<and> (\<forall>i\<in>agents. U[i] (\<X> i) \<le> U[i] (Y i)) \<and> (\<exists>i\<in>agents. U[i] (\<X> i) < U[i] (Y i))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i \<in> agents; U[i] (\<X> i) < U[i] (Y i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i \<in> agents
U[i] (\<X> i) < U[i] (Y i)

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>agents. Price \<bullet> \<X> i < Price \<bullet> Y i) \<Longrightarrow> False
[PROOF STEP]
have "Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i
[PROOF STEP]
have "Price \<bullet> Y i > Price \<bullet> \<E> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Price \<bullet> \<E>[i] < Price \<bullet> Y i
[PROOF STEP]
by (metis pref_more_expensive comp_equilib_endow_def
            equilibrium inner_commute obt_witness(1) obt_witness(2))
[PROOF STATE]
proof (state)
this:
Price \<bullet> \<E>[i] < Price \<bullet> Y i

goal (1 subgoal):
 1. Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i
[PROOF STEP]
have "Price \<bullet> \<E> i = Price \<bullet> \<X> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Price \<bullet> \<E>[i] = Price \<bullet> \<X> i
[PROOF STEP]
using equilibrium lns obt_witness(1) walras_law_per_agent
[PROOF STATE]
proof (prove)
using this:
comp_equilib_endow Price \<X> \<E>
?i1 \<in> agents \<Longrightarrow> local_nonsatiation consumption_set Pr[?i1]
i \<in> agents
\<lbrakk>\<And>i. i \<in> agents \<Longrightarrow> local_nonsatiation consumption_set Pr[i]; comp_equilib_endow ?P ?X \<E>\<rbrakk> \<Longrightarrow> \<forall>i\<in>agents. ?P \<bullet> ?X i = ?P \<bullet> \<E>[i]

goal (1 subgoal):
 1. Price \<bullet> \<E>[i] = Price \<bullet> \<X> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Price \<bullet> \<E>[i] = Price \<bullet> \<X> i

goal (1 subgoal):
 1. Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Price \<bullet> \<E>[i] = Price \<bullet> \<X> i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Price \<bullet> \<E>[i] = Price \<bullet> \<X> i

goal (1 subgoal):
 1. Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i
[PROOF STEP]
using \<open>Price \<bullet> \<E> i < Price \<bullet> Y i\<close>
[PROOF STATE]
proof (prove)
using this:
Price \<bullet> \<E>[i] = Price \<bullet> \<X> i
Price \<bullet> \<E>[i] < Price \<bullet> Y i

goal (1 subgoal):
 1. Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i

goal (1 subgoal):
 1. \<not> (\<exists>i\<in>agents. Price \<bullet> \<X> i < Price \<bullet> Y i) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i

goal (1 subgoal):
 1. False
[PROOF STEP]
using a1 all_great_eq_value obt_witness(1)
[PROOF STATE]
proof (prove)
using this:
Price \<bullet> Y i \<noteq> Price \<bullet> \<X> i
\<not> (\<exists>i\<in>agents. Price \<bullet> \<X> i < Price \<bullet> Y i)
\<forall>i\<in>agents. Price \<bullet> \<X> i \<le> Price \<bullet> Y i
i \<in> agents

goal (1 subgoal):
 1. False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>agents. Price \<bullet> \<X> i < Price \<bullet> Y i

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
have dominating_more_exp : "Price \<bullet> (\<Sum>i\<in>agents. Y i) > Price \<bullet> (\<Sum>i\<in>agents. \<X> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents
[PROOF STEP]
have mp_rule : "(\<Sum>i\<in>agents. Price \<bullet> Y i) > (\<Sum>i\<in>agents. Price \<bullet> \<X> i) \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>agents. Price \<bullet> \<X> i) < (\<Sum>i\<in>agents. Price \<bullet> Y i) \<Longrightarrow> Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents
[PROOF STEP]
by (simp add: inner_sum_right)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>agents. Price \<bullet> \<X> i) < (\<Sum>i\<in>agents. Price \<bullet> Y i) \<Longrightarrow> Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents

goal (1 subgoal):
 1. Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents
[PROOF STEP]
have "(\<Sum>i\<in>agents. Price \<bullet> Y i) > (\<Sum>i\<in>agents. Price \<bullet> \<X> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>agents. Price \<bullet> \<X> i) < (\<Sum>i\<in>agents. Price \<bullet> Y i)
[PROOF STEP]
by (simp add: all_great_eq_value finite_agents ex_greater_value sum_strict_mono_ex1)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>agents. Price \<bullet> \<X> i) < (\<Sum>i\<in>agents. Price \<bullet> Y i)

goal (1 subgoal):
 1. Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents
[PROOF STEP]
thus "Price \<bullet> (\<Sum>i\<in>agents. Y i) > Price \<bullet> (\<Sum>i\<in>agents. \<X> i)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>agents. Price \<bullet> \<X> i) < (\<Sum>i\<in>agents. Price \<bullet> Y i)

goal (1 subgoal):
 1. Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents
[PROOF STEP]
using mp_rule
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>agents. Price \<bullet> \<X> i) < (\<Sum>i\<in>agents. Price \<bullet> Y i)
(\<Sum>i\<in>agents. Price \<bullet> \<X> i) < (\<Sum>i\<in>agents. Price \<bullet> Y i) \<Longrightarrow> Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents

goal (1 subgoal):
 1. Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
have equili_walras_law : "Price \<bullet> (\<Sum>i\<in>agents. \<X> i) = Price \<bullet> (\<Sum>i\<in>agents. \<E>[i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Price \<bullet> sum \<X> agents = Price \<bullet> sum \<E> agents
[PROOF STEP]
by (metis (mono_tags) eq_iff_diff_eq_0 equilibrium
        inner_sum_right lns walras_law)
[PROOF STATE]
proof (state)
this:
Price \<bullet> sum \<X> agents = Price \<bullet> sum \<E> agents

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
have dominating_feasible : "Price \<bullet> (\<Sum>i\<in>agents. \<X> i) \<ge> Price \<bullet> (\<Sum>i\<in>agents. Y i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Price \<bullet> sum Y agents \<le> Price \<bullet> sum \<X> agents
[PROOF STEP]
by (metis atLeastAtMost_iff dual_order.order_iff_strict equili_walras_law
        feasible_allocation_def inner_commute interval_inner_leI(1) is_feasible price_g_zero)
[PROOF STATE]
proof (state)
this:
Price \<bullet> sum Y agents \<le> Price \<bullet> sum \<X> agents

goal (1 subgoal):
 1. \<not> pareto_optimal_endow \<X> \<E> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using dominating_more_exp equili_walras_law dominating_feasible
[PROOF STATE]
proof (prove)
using this:
Price \<bullet> sum \<X> agents < Price \<bullet> sum Y agents
Price \<bullet> sum \<X> agents = Price \<bullet> sum \<E> agents
Price \<bullet> sum Y agents \<le> Price \<bullet> sum \<X> agents

goal (1 subgoal):
 1. False
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chop_rule: "reducing splitf \<Longrightarrow>
  chop splitf xs = (let (pre, post) = splitf xs
                    in if pre = [] then ([], xs)
                       else let (xss, zs) = chop splitf post
                            in (pre # xss,zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reducing splitf \<Longrightarrow> chop splitf xs = (let (pre, post) = splitf xs in if pre = [] then ([], xs) else let (xss, zs) = chop splitf post in (pre # xss, zs))
[PROOF STEP]
apply (simp add: chop.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reducing splitf \<Longrightarrow> (let pp = splitf xs in if fst pp = [] then ([], xs) else let qq = chop splitf (snd pp) in (fst pp # fst qq, snd qq)) = (case splitf xs of (pre, post) \<Rightarrow> if pre = [] then ([], xs) else let (xss, y) = chop splitf post in (pre # xss, y))
[PROOF STEP]
apply (simp add: Let_def split: prod.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma reducing_maxsplit: "reducing(\<lambda>qs. maxsplit P ([],qs) [] qs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reducing (\<lambda>qs. maxsplit P ([], qs) [] qs)
[PROOF STEP]
by (simp add: reducing_def maxsplit_eq)


[STATEMENT]
lemma is_maxsplitter_reducing:
 "is_maxsplitter P splitf \<Longrightarrow> reducing splitf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_maxsplitter P splitf \<Longrightarrow> reducing splitf
[PROOF STEP]
by(simp add:is_maxsplitter_def reducing_def)


[STATEMENT]
lemma chop_concat[rule_format]: "is_maxsplitter P splitf \<Longrightarrow>
  (\<forall>yss zs. chop splitf xs = (yss,zs) \<longrightarrow> xs = concat yss @ zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_maxsplitter P splitf \<Longrightarrow> \<forall>yss zs. chop splitf xs = (yss, zs) \<longrightarrow> xs = concat yss @ zs
[PROOF STEP]
apply (induct xs rule:length_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> is_maxsplitter P splitf \<longrightarrow> (\<forall>yss zs. chop splitf ys = (yss, zs) \<longrightarrow> ys = concat yss @ zs); is_maxsplitter P splitf\<rbrakk> \<Longrightarrow> \<forall>yss zs. chop splitf xs = (yss, zs) \<longrightarrow> xs = concat yss @ zs
[PROOF STEP]
apply (simp (no_asm_simp) split del: if_split
            add: chop_rule[OF is_maxsplitter_reducing])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> is_maxsplitter P splitf \<longrightarrow> (\<forall>yss zs. chop splitf ys = (yss, zs) \<longrightarrow> ys = concat yss @ zs); is_maxsplitter P splitf\<rbrakk> \<Longrightarrow> \<forall>yss zs. (case splitf xs of (pre, post) \<Rightarrow> if pre = [] then ([], xs) else let (xss, y) = chop splitf post in (pre # xss, y)) = (yss, zs) \<longrightarrow> xs = concat yss @ zs
[PROOF STEP]
apply (simp add: Let_def is_maxsplitter_def split: prod.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma chop_nonempty: "is_maxsplitter P splitf \<Longrightarrow>
  \<forall>yss zs. chop splitf xs = (yss,zs) \<longrightarrow> (\<forall>ys \<in> set yss. ys \<noteq> [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_maxsplitter P splitf \<Longrightarrow> \<forall>yss zs. chop splitf xs = (yss, zs) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])
[PROOF STEP]
apply (induct xs rule:length_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> is_maxsplitter P splitf \<longrightarrow> (\<forall>yss zs. chop splitf ys = (yss, zs) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])); is_maxsplitter P splitf\<rbrakk> \<Longrightarrow> \<forall>yss zs. chop splitf xs = (yss, zs) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])
[PROOF STEP]
apply (simp (no_asm_simp) add: chop_rule is_maxsplitter_reducing)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> is_maxsplitter P splitf \<longrightarrow> (\<forall>yss zs. chop splitf ys = (yss, zs) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])); is_maxsplitter P splitf\<rbrakk> \<Longrightarrow> \<forall>yss. (\<exists>zs. (case splitf xs of (pre, post) \<Rightarrow> if pre = [] then ([], xs) else let (xss, y) = chop splitf post in (pre # xss, y)) = (yss, zs)) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])
[PROOF STEP]
apply (simp add: Let_def is_maxsplitter_def split: prod.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>yss. (\<exists>zs. chop splitf ys = (yss, zs)) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])); \<forall>xs ps qs. (splitf xs = (ps, qs)) = (xs = ps @ qs \<and> is_maxpref P ps xs)\<rbrakk> \<Longrightarrow> \<forall>x1. x1 \<noteq> [] \<longrightarrow> (\<forall>x2 x1a. (\<exists>x2a. chop splitf x2 = (x1a, x2a)) \<longrightarrow> xs = x1 @ x2 \<and> is_maxpref P x1 xs \<longrightarrow> (\<forall>ys\<in>set x1a. ys \<noteq> []))
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs x1 x2 x1a. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>yss. (\<exists>zs. chop splitf ys = (yss, zs)) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])); \<forall>xs ps qs. (splitf xs = (ps, qs)) = (xs = ps @ qs \<and> is_maxpref P ps xs); x1 \<noteq> []; \<exists>x2a. chop splitf x2 = (x1a, x2a); xs = x1 @ x2 \<and> is_maxpref P x1 xs\<rbrakk> \<Longrightarrow> \<forall>ys\<in>set x1a. ys \<noteq> []
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs x1 x2 x1a ys. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>yss. (\<exists>zs. chop splitf ys = (yss, zs)) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])); \<forall>xs ps qs. (splitf xs = (ps, qs)) = (xs = ps @ qs \<and> is_maxpref P ps xs); x1 \<noteq> []; \<exists>x2a. chop splitf x2 = (x1a, x2a); xs = x1 @ x2 \<and> is_maxpref P x1 xs; ys \<in> set x1a\<rbrakk> \<Longrightarrow> ys \<noteq> []
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs x1 x2 x1a ys x2a. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>yss. (\<exists>zs. chop splitf ys = (yss, zs)) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> [])); \<forall>xs ps qs. (splitf xs = (ps, qs)) = (xs = ps @ qs \<and> is_maxpref P ps xs); x1 \<noteq> []; xs = x1 @ x2 \<and> is_maxpref P x1 xs; ys \<in> set x1a; chop splitf x2 = (x1a, x2a)\<rbrakk> \<Longrightarrow> ys \<noteq> []
[PROOF STEP]
apply (erule allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs x1 x2 x1a ys x2a. \<lbrakk>\<forall>xs ps qs. (splitf xs = (ps, qs)) = (xs = ps @ qs \<and> is_maxpref P ps xs); x1 \<noteq> []; xs = x1 @ x2 \<and> is_maxpref P x1 xs; ys \<in> set x1a; chop splitf x2 = (x1a, x2a); length (?ys43 xs x1 x2 x1a ys x2a) < length xs \<longrightarrow> (\<forall>yss. (\<exists>zs. chop splitf (?ys43 xs x1 x2 x1a ys x2a) = (yss, zs)) \<longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> []))\<rbrakk> \<Longrightarrow> ys \<noteq> []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_maxchopper_chop:
 assumes prem: "is_maxsplitter P splitf" shows "is_maxchopper P (chop splitf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_maxchopper P (chop splitf)
[PROOF STEP]
apply(unfold is_maxchopper_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs zs yss. (chop splitf xs = (yss, zs)) = (xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)))
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs zs yss. (chop splitf xs = (yss, zs)) = (xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)))
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss. chop splitf xs = (yss, zs) \<Longrightarrow> xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs))
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs zs yss. chop splitf xs = (yss, zs) \<Longrightarrow> xs = concat yss @ zs
 2. \<And>xs zs yss. chop splitf xs = (yss, zs) \<Longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs))
 3. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (erule chop_concat[OF prem])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss. chop splitf xs = (yss, zs) \<Longrightarrow> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs))
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs zs yss. chop splitf xs = (yss, zs) \<Longrightarrow> \<forall>ys\<in>set yss. ys \<noteq> []
 2. \<And>xs zs yss. chop splitf xs = (yss, zs) \<Longrightarrow> case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)
 3. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (erule prem[THEN chop_nonempty[THEN spec, THEN spec, THEN mp]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss. chop splitf xs = (yss, zs) \<Longrightarrow> case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss. chop splitf xs = (yss, zs) \<longrightarrow> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs))
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (subst prem[THEN is_maxsplitter_reducing[THEN chop_rule]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss. (let (pre, post) = splitf xs in if pre = [] then ([], xs) else let (xss, y) = chop splitf post in (pre # xss, y)) = (yss, zs) \<longrightarrow> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs))
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (simp add: Let_def prem[simplified is_maxsplitter_def]
             split: prod.split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss. \<forall>x1 x2 x1a x2a. chop splitf x2 = (x1a, x2a) \<longrightarrow> (x1 = [] \<longrightarrow> xs = x2 \<and> is_maxpref P [] xs \<longrightarrow> [] = yss \<and> x2 = zs \<longrightarrow> is_maxpref P [] zs) \<and> (x1 \<noteq> [] \<longrightarrow> xs = x1 @ x2 \<and> is_maxpref P x1 xs \<longrightarrow> x1 # x1a = yss \<and> x2a = zs \<longrightarrow> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)))
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss x1 x2 x1a x2a. chop splitf x2 = (x1a, x2a) \<Longrightarrow> (x1 = [] \<longrightarrow> xs = x2 \<and> is_maxpref P [] xs \<longrightarrow> [] = yss \<and> x2 = zs \<longrightarrow> is_maxpref P [] zs) \<and> (x1 \<noteq> [] \<longrightarrow> xs = x1 @ x2 \<and> is_maxpref P x1 xs \<longrightarrow> x1 # x1a = yss \<and> x2a = zs \<longrightarrow> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)))
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xs zs yss x1 x2 x1a x2a. chop splitf x2 = (x1a, x2a) \<Longrightarrow> x1 = [] \<longrightarrow> xs = x2 \<and> is_maxpref P [] xs \<longrightarrow> [] = yss \<and> x2 = zs \<longrightarrow> is_maxpref P [] zs
 2. \<And>xs zs yss x1 x2 x1a x2a. chop splitf x2 = (x1a, x2a) \<Longrightarrow> x1 \<noteq> [] \<longrightarrow> xs = x1 @ x2 \<and> is_maxpref P x1 xs \<longrightarrow> x1 # x1a = yss \<and> x2a = zs \<longrightarrow> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs))
 3. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss x1 x2 x1a x2a. chop splitf x2 = (x1a, x2a) \<Longrightarrow> x1 \<noteq> [] \<longrightarrow> xs = x1 @ x2 \<and> is_maxpref P x1 xs \<longrightarrow> x1 # x1a = yss \<and> x2a = zs \<longrightarrow> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs))
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs zs yss x1 x2 x1a x2a. \<lbrakk>chop splitf x2 = (x1a, zs); x1 \<noteq> []; is_maxpref P x1 (x1 @ x2)\<rbrakk> \<Longrightarrow> case x1 # x1a of [] \<Rightarrow> is_maxpref P [] (x1 @ x2) | us # uss \<Rightarrow> is_maxpref P us (x1 @ x2) \<and> chop splitf (concat uss @ zs) = (uss, zs)
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs x1 x2 x1a. \<lbrakk>chop splitf x2 = (x1a, zs); x1 \<noteq> []; is_maxpref P x1 (x1 @ x2)\<rbrakk> \<Longrightarrow> chop splitf (concat x1a @ zs) = (x1a, zs)
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (frule chop_concat[OF prem])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs x1 x2 x1a. \<lbrakk>chop splitf x2 = (x1a, zs); x1 \<noteq> []; is_maxpref P x1 (x1 @ x2); x2 = concat x1a @ zs\<rbrakk> \<Longrightarrow> chop splitf (concat x1a @ zs) = (x1a, zs)
 2. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> chop splitf xs = (yss, zs)
[PROOF STEP]
apply (subst prem[THEN is_maxsplitter_reducing, THEN chop_rule])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs zs yss. xs = concat yss @ zs \<and> (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] xs | us # uss \<Rightarrow> is_maxpref P us xs \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> (let (pre, post) = splitf xs in if pre = [] then ([], xs) else let (xss, y) = chop splitf post in (pre # xss, y)) = (yss, zs)
[PROOF STEP]
apply (simp add: Let_def prem[simplified is_maxsplitter_def]
             split: prod.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs yss. (\<forall>ys\<in>set yss. ys \<noteq> []) \<and> (case yss of [] \<Rightarrow> is_maxpref P [] (concat yss @ zs) | us # uss \<Rightarrow> is_maxpref P us (concat yss @ zs) \<and> chop splitf (concat uss @ zs) = (uss, zs)) \<Longrightarrow> \<forall>x1 x2 x1a x2a. chop splitf x2 = (x1a, x2a) \<longrightarrow> (x1 = [] \<longrightarrow> concat yss @ zs = x2 \<and> is_maxpref P [] (concat yss @ zs) \<longrightarrow> [] = yss \<and> x2 = zs) \<and> (x1 \<noteq> [] \<longrightarrow> concat yss @ zs = x1 @ x2 \<and> is_maxpref P x1 (concat yss @ zs) \<longrightarrow> x1 # x1a = yss \<and> x2a = zs)
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs yss x1 x2 x1a x2a. \<lbrakk>\<forall>ys\<in>set yss. ys \<noteq> []; case yss of [] \<Rightarrow> is_maxpref P [] (concat yss @ zs) | us # uss \<Rightarrow> is_maxpref P us (concat yss @ zs) \<and> chop splitf (concat uss @ zs) = (uss, zs); chop splitf x2 = (x1a, x2a)\<rbrakk> \<Longrightarrow> (x1 = [] \<longrightarrow> concat yss @ zs = x2 \<and> is_maxpref P [] (concat yss @ zs) \<longrightarrow> [] = yss \<and> x2 = zs) \<and> (x1 \<noteq> [] \<longrightarrow> concat yss @ zs = x1 @ x2 \<and> is_maxpref P x1 (concat yss @ zs) \<longrightarrow> x1 # x1a = yss \<and> x2a = zs)
[PROOF STEP]
apply (rename_tac xs1 ys1 xss1 ys)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs yss xs1 ys1 xss1 ys. \<lbrakk>\<forall>ys\<in>set yss. ys \<noteq> []; case yss of [] \<Rightarrow> is_maxpref P [] (concat yss @ zs) | us # uss \<Rightarrow> is_maxpref P us (concat yss @ zs) \<and> chop splitf (concat uss @ zs) = (uss, zs); chop splitf ys1 = (xss1, ys)\<rbrakk> \<Longrightarrow> (xs1 = [] \<longrightarrow> concat yss @ zs = ys1 \<and> is_maxpref P [] (concat yss @ zs) \<longrightarrow> [] = yss \<and> ys1 = zs) \<and> (xs1 \<noteq> [] \<longrightarrow> concat yss @ zs = xs1 @ ys1 \<and> is_maxpref P xs1 (concat yss @ zs) \<longrightarrow> xs1 # xss1 = yss \<and> ys = zs)
[PROOF STEP]
apply (simp split: list.split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs yss xs1 ys1 xss1 ys. \<lbrakk>chop splitf ys1 = (xss1, ys); yss = []; is_maxpref P [] zs\<rbrakk> \<Longrightarrow> xs1 \<noteq> [] \<longrightarrow> zs = xs1 @ ys1 \<longrightarrow> \<not> is_maxpref P xs1 (xs1 @ ys1)
 2. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> [] \<and> (\<forall>ys\<in>set x22. ys \<noteq> []); yss = x21 # x22; is_maxpref P x21 (x21 @ concat x22 @ zs) \<and> chop splitf (concat x22 @ zs) = (x22, zs)\<rbrakk> \<Longrightarrow> (xs1 = [] \<longrightarrow> x21 @ concat x22 @ zs = ys1 \<longrightarrow> \<not> is_maxpref P [] ys1) \<and> (xs1 \<noteq> [] \<longrightarrow> x21 @ concat x22 @ zs = xs1 @ ys1 \<and> is_maxpref P xs1 (x21 @ concat x22 @ zs) \<longrightarrow> xs1 = x21 \<and> xss1 = x22 \<and> ys = zs)
[PROOF STEP]
apply (simp add: is_maxpref_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs yss xs1 ys1 xss1 ys. \<lbrakk>chop splitf ys1 = (xss1, ys); yss = []; \<forall>zsa. prefix zsa zs \<and> P zsa \<longrightarrow> zsa = []\<rbrakk> \<Longrightarrow> xs1 \<noteq> [] \<longrightarrow> zs = xs1 @ ys1 \<longrightarrow> P xs1 \<longrightarrow> (\<exists>zs. prefix zs (xs1 @ ys1) \<and> P zs \<and> \<not> prefix zs xs1)
 2. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> [] \<and> (\<forall>ys\<in>set x22. ys \<noteq> []); yss = x21 # x22; is_maxpref P x21 (x21 @ concat x22 @ zs) \<and> chop splitf (concat x22 @ zs) = (x22, zs)\<rbrakk> \<Longrightarrow> (xs1 = [] \<longrightarrow> x21 @ concat x22 @ zs = ys1 \<longrightarrow> \<not> is_maxpref P [] ys1) \<and> (xs1 \<noteq> [] \<longrightarrow> x21 @ concat x22 @ zs = xs1 @ ys1 \<and> is_maxpref P xs1 (x21 @ concat x22 @ zs) \<longrightarrow> xs1 = x21 \<and> xss1 = x22 \<and> ys = zs)
[PROOF STEP]
apply (blast intro: prefix_append[THEN iffD2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> [] \<and> (\<forall>ys\<in>set x22. ys \<noteq> []); yss = x21 # x22; is_maxpref P x21 (x21 @ concat x22 @ zs) \<and> chop splitf (concat x22 @ zs) = (x22, zs)\<rbrakk> \<Longrightarrow> (xs1 = [] \<longrightarrow> x21 @ concat x22 @ zs = ys1 \<longrightarrow> \<not> is_maxpref P [] ys1) \<and> (xs1 \<noteq> [] \<longrightarrow> x21 @ concat x22 @ zs = xs1 @ ys1 \<and> is_maxpref P xs1 (x21 @ concat x22 @ zs) \<longrightarrow> xs1 = x21 \<and> xss1 = x22 \<and> ys = zs)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> [] \<and> (\<forall>ys\<in>set x22. ys \<noteq> []); yss = x21 # x22; is_maxpref P x21 (x21 @ concat x22 @ zs) \<and> chop splitf (concat x22 @ zs) = (x22, zs)\<rbrakk> \<Longrightarrow> xs1 = [] \<longrightarrow> x21 @ concat x22 @ zs = ys1 \<longrightarrow> \<not> is_maxpref P [] ys1
 2. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> [] \<and> (\<forall>ys\<in>set x22. ys \<noteq> []); yss = x21 # x22; is_maxpref P x21 (x21 @ concat x22 @ zs) \<and> chop splitf (concat x22 @ zs) = (x22, zs)\<rbrakk> \<Longrightarrow> xs1 \<noteq> [] \<longrightarrow> x21 @ concat x22 @ zs = xs1 @ ys1 \<and> is_maxpref P xs1 (x21 @ concat x22 @ zs) \<longrightarrow> xs1 = x21 \<and> xss1 = x22 \<and> ys = zs
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf (x21 @ concat x22 @ zs) = (xss1, ys); x21 \<noteq> []; \<forall>ys\<in>set x22. ys \<noteq> []; is_maxpref P x21 (x21 @ concat x22 @ zs); chop splitf (concat x22 @ zs) = (x22, zs); is_maxpref P [] (x21 @ concat x22 @ zs)\<rbrakk> \<Longrightarrow> False
 2. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> [] \<and> (\<forall>ys\<in>set x22. ys \<noteq> []); yss = x21 # x22; is_maxpref P x21 (x21 @ concat x22 @ zs) \<and> chop splitf (concat x22 @ zs) = (x22, zs)\<rbrakk> \<Longrightarrow> xs1 \<noteq> [] \<longrightarrow> x21 @ concat x22 @ zs = xs1 @ ys1 \<and> is_maxpref P xs1 (x21 @ concat x22 @ zs) \<longrightarrow> xs1 = x21 \<and> xss1 = x22 \<and> ys = zs
[PROOF STEP]
apply (simp (no_asm_use) add: is_maxpref_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs xss1 ys x21 x22. \<lbrakk>chop splitf (x21 @ concat x22 @ zs) = (xss1, ys); x21 \<noteq> []; \<forall>ys\<in>set x22. ys \<noteq> []; (x21 = [] \<or> P x21) \<and> (\<forall>zsa. prefix zsa (x21 @ concat x22 @ zs) \<and> P zsa \<longrightarrow> prefix zsa x21); chop splitf (concat x22 @ zs) = (x22, zs); \<forall>zsa. prefix zsa (x21 @ concat x22 @ zs) \<and> P zsa \<longrightarrow> zsa = []\<rbrakk> \<Longrightarrow> False
 2. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> [] \<and> (\<forall>ys\<in>set x22. ys \<noteq> []); yss = x21 # x22; is_maxpref P x21 (x21 @ concat x22 @ zs) \<and> chop splitf (concat x22 @ zs) = (x22, zs)\<rbrakk> \<Longrightarrow> xs1 \<noteq> [] \<longrightarrow> x21 @ concat x22 @ zs = xs1 @ ys1 \<and> is_maxpref P xs1 (x21 @ concat x22 @ zs) \<longrightarrow> xs1 = x21 \<and> xss1 = x22 \<and> ys = zs
[PROOF STEP]
apply (blast intro: prefix_append[THEN iffD2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> [] \<and> (\<forall>ys\<in>set x22. ys \<noteq> []); yss = x21 # x22; is_maxpref P x21 (x21 @ concat x22 @ zs) \<and> chop splitf (concat x22 @ zs) = (x22, zs)\<rbrakk> \<Longrightarrow> xs1 \<noteq> [] \<longrightarrow> x21 @ concat x22 @ zs = xs1 @ ys1 \<and> is_maxpref P xs1 (x21 @ concat x22 @ zs) \<longrightarrow> xs1 = x21 \<and> xss1 = x22 \<and> ys = zs
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs yss xs1 ys1 xss1 ys x21 x22. \<lbrakk>chop splitf ys1 = (xss1, ys); x21 \<noteq> []; \<forall>ys\<in>set x22. ys \<noteq> []; is_maxpref P x21 (x21 @ concat x22 @ zs); chop splitf (concat x22 @ zs) = (x22, zs); xs1 \<noteq> []; x21 @ concat x22 @ zs = xs1 @ ys1; is_maxpref P xs1 (x21 @ concat x22 @ zs)\<rbrakk> \<Longrightarrow> xs1 = x21 \<and> xss1 = x22 \<and> ys = zs
[PROOF STEP]
apply (rename_tac us uss)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs yss xs1 ys1 xss1 ys us uss. \<lbrakk>chop splitf ys1 = (xss1, ys); us \<noteq> []; \<forall>ys\<in>set uss. ys \<noteq> []; is_maxpref P us (us @ concat uss @ zs); chop splitf (concat uss @ zs) = (uss, zs); xs1 \<noteq> []; us @ concat uss @ zs = xs1 @ ys1; is_maxpref P xs1 (us @ concat uss @ zs)\<rbrakk> \<Longrightarrow> xs1 = us \<and> xss1 = uss \<and> ys = zs
[PROOF STEP]
apply (subgoal_tac "xs1=us")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>zs yss xs1 ys1 xss1 ys us uss. \<lbrakk>chop splitf ys1 = (xss1, ys); us \<noteq> []; \<forall>ys\<in>set uss. ys \<noteq> []; is_maxpref P us (us @ concat uss @ zs); chop splitf (concat uss @ zs) = (uss, zs); xs1 \<noteq> []; us @ concat uss @ zs = xs1 @ ys1; is_maxpref P xs1 (us @ concat uss @ zs); xs1 = us\<rbrakk> \<Longrightarrow> xs1 = us \<and> xss1 = uss \<and> ys = zs
 2. \<And>zs yss xs1 ys1 xss1 ys us uss. \<lbrakk>chop splitf ys1 = (xss1, ys); us \<noteq> []; \<forall>ys\<in>set uss. ys \<noteq> []; is_maxpref P us (us @ concat uss @ zs); chop splitf (concat uss @ zs) = (uss, zs); xs1 \<noteq> []; us @ concat uss @ zs = xs1 @ ys1; is_maxpref P xs1 (us @ concat uss @ zs)\<rbrakk> \<Longrightarrow> xs1 = us
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs yss xs1 ys1 xss1 ys us uss. \<lbrakk>chop splitf ys1 = (xss1, ys); us \<noteq> []; \<forall>ys\<in>set uss. ys \<noteq> []; is_maxpref P us (us @ concat uss @ zs); chop splitf (concat uss @ zs) = (uss, zs); xs1 \<noteq> []; us @ concat uss @ zs = xs1 @ ys1; is_maxpref P xs1 (us @ concat uss @ zs)\<rbrakk> \<Longrightarrow> xs1 = us
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs xs1 ys1 xss1 ys us uss. \<lbrakk>chop splitf ys1 = (xss1, ys); us \<noteq> []; \<forall>ys\<in>set uss. ys \<noteq> []; is_maxpref P us (xs1 @ ys1); chop splitf (concat uss @ zs) = (uss, zs); xs1 \<noteq> []; us @ concat uss @ zs = xs1 @ ys1; is_maxpref P xs1 (xs1 @ ys1)\<rbrakk> \<Longrightarrow> xs1 = us
[PROOF STEP]
apply (simp (no_asm_use) add: is_maxpref_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>zs xs1 ys1 xss1 ys us uss. \<lbrakk>chop splitf ys1 = (xss1, ys); us \<noteq> []; \<forall>ys\<in>set uss. ys \<noteq> []; prefix us (xs1 @ ys1) \<and> (us = [] \<or> P us) \<and> (\<forall>zs. prefix zs (xs1 @ ys1) \<and> P zs \<longrightarrow> prefix zs us); chop splitf (concat uss @ zs) = (uss, zs); xs1 \<noteq> []; us @ concat uss @ zs = xs1 @ ys1; (xs1 = [] \<or> P xs1) \<and> (\<forall>zs. prefix zs (xs1 @ ys1) \<and> P zs \<longrightarrow> prefix zs xs1)\<rbrakk> \<Longrightarrow> xs1 = us
[PROOF STEP]
apply (blast intro: prefix_append[THEN iffD2] prefix_order.antisym)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma geometric_spmf_fixp_induct [case_names adm bottom step]:
  assumes "spmf.admissible P"
    and "P (\<lambda>geometric_spmf. return_pmf None)"
    and "\<And>geometric_spmf'. P geometric_spmf' \<Longrightarrow> P (\<lambda>p. bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (geometric_spmf' p)))"
  shows "P geometric_spmf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P geometric_spmf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
spmf.admissible P
P (\<lambda>geometric_spmf. return_pmf None)
P ?geometric_spmf' \<Longrightarrow> P (\<lambda>p. bernoulli p \<bind> (\<lambda>b. if b then return_spmf 0 else map_spmf ((+) 1) (?geometric_spmf' p)))

goal (1 subgoal):
 1. P geometric_spmf
[PROOF STEP]
by(rule geometric_spmf.fixp_induct)


[STATEMENT]
lemma spmf_geometric_nonpos: "p \<le> 0 \<Longrightarrow> geometric_spmf p = return_pmf None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> 0 \<Longrightarrow> geometric_spmf p = return_pmf None
[PROOF STEP]
by(induction rule: geometric_spmf_fixp_induct) simp_all


[STATEMENT]
lemma spmf_geometric_ge_1: "1 \<le> p \<Longrightarrow> geometric_spmf p = return_spmf 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> p \<Longrightarrow> geometric_spmf p = return_spmf 0
[PROOF STEP]
by(simp add: geometric_spmf.simps)