[STATEMENT]
lemma effect_swapE [effect_elims]:
  assumes "effect (swap i x a) h h' r n"
  obtains "r = get h a ! i" "h' = update a i x h" "i < length h a" "n=2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = get h a ! i; h' = update a i x h; i < Array_Time.length h a; n = 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (swap i x a) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>r = get h a ! i; h' = update a i x h; i < Array_Time.length h a; n = 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)


[STATEMENT]
lemma execute_freeze [execute_simps]:
  "execute (freeze a) h = Some (get h a, h, 1+length h a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (freeze a) h = Some (get h a, h, 1 + Array_Time.length h a)
[PROOF STEP]
by (simp add: freeze_def execute_simps)


[STATEMENT]
lemma success_freezeI [success_intros]:
  "success (freeze a) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (freeze a) h
[PROOF STEP]
by (auto intro: success_intros simp add: freeze_def)


[STATEMENT]
lemma effect_freezeI [effect_intros]:
  assumes "h' = h" "r = get h a" "n=length h a"
  shows "effect (freeze a) h h' r (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (freeze a) h h' r (n + 1)
[PROOF STEP]
by (rule effectI) (insert assms, simp add: execute_simps)


[STATEMENT]
lemma effect_freezeE [effect_elims]:
  assumes "effect (freeze a) h h' r n"
  obtains "h' = h" "r = get h a" "n=length h a+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>h' = h; r = get h a; n = Array_Time.length h a + 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (freeze a) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>h' = h; r = get h a; n = Array_Time.length h a + 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (simp add: execute_simps)


[STATEMENT]
lemma upd_ureturn:
  "upd i x a \<then> ureturn a =   upd i x a "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upd i x a \<bind> (\<lambda>_. ureturn a) = upd i x a
[PROOF STEP]
by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps)


[STATEMENT]
lemma array_make:
  "new n x = make n (\<lambda>_. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new n x = Array_Time.make n (\<lambda>_. x)
[PROOF STEP]
by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps)


[STATEMENT]
lemma array_of_list_make [code]:
  "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_list xs = Array_Time.make (List.length xs) ((!) xs)
[PROOF STEP]
by (rule Heap_eqI) (simp add: map_nth execute_simps)


[STATEMENT]
lemma [code]:
  "Array_Time.new = new' o of_nat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.new = new' \<circ> of_nat
[PROOF STEP]
by (simp add: new'_def o_def)


[STATEMENT]
lemma [code]:
  "Array_Time.make n f = make' (of_nat n) (f o nat_of_integer)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.make n f = make' (of_nat n) (f \<circ> nat_of_integer)
[PROOF STEP]
by (simp add: make'_def o_def)


[STATEMENT]
lemma [code]:
  "Array_Time.len a = len' a \<bind> (\<lambda>i. ureturn (nat_of_integer i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.len a = len' a \<bind> (\<lambda>i. ureturn (nat_of_integer i))
[PROOF STEP]
by (simp add: len'_def execute_simps)


[STATEMENT]
lemma [code]:
  "Array_Time.nth a n = nth' a (of_nat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.nth a n = nth' a (of_nat n)
[PROOF STEP]
by (simp add: nth'_def)


[STATEMENT]
lemma [code]:
  "Array_Time.upd i x a = upd' a (of_nat i) x \<then> ureturn a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.upd i x a = upd' a (of_nat i) x \<bind> (\<lambda>_. ureturn a)
[PROOF STEP]
by (simp add: upd'_def upd_ureturn execute_simps)


[STATEMENT]
lemma [code]:
  "Array_Time.map_entry i f a = do {
     x \<leftarrow> Array_Time.nth a i;
     Array_Time.upd i (f x) a
   }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.map_entry i f a = Array_Time.nth a i \<bind> (\<lambda>x. Array_Time.upd i (f x) a)
[PROOF STEP]
by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)


[STATEMENT]
lemma [code]:
  "Array_Time.swap i x a = do {
     y \<leftarrow> Array_Time.nth a i;
     Array_Time.upd i x a;
     ureturn y
   }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.swap i x a = Array_Time.nth a i \<bind> (\<lambda>y. Array_Time.upd i x a \<bind> (\<lambda>_. ureturn y))
[PROOF STEP]
by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)


[STATEMENT]
lemma src_port: "src_port (a,x::adr\<^sub>i\<^sub>p\<^sub>p,d,e) = fst (snd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. src_port (a, x, d, e) = fst (snd x)
[PROOF STEP]
by (simp add: src_port_int_TCPUDP_def in_subnet)


[STATEMENT]
lemma dest_port: "dest_port (a,d,x::adr\<^sub>i\<^sub>p\<^sub>p,e) = fst (snd x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dest_port (a, d, x, e) = fst (snd x)
[PROOF STEP]
by (simp add: dest_port_int_TCPUDP_def in_subnet)


[STATEMENT]
lemma add_bot_bot_bot:
  "x + bot + bot + bot = x + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + bot + bot + bot = x + bot
[PROOF STEP]
by simp


[STATEMENT]
lemma agg_sum_bot:
  "(\<Sum>\<^sub>k bot::'a::aggregation_order) = bot + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. bot) {k. True} = zero
[PROOF STEP]
proof (induct rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. infinite A \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) A = zero
 2. aggregation.sum_0 (\<lambda>k. bot) {} = zero
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; aggregation.sum_0 (\<lambda>k. bot) F = zero\<rbrakk> \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
case (infinite A)
[PROOF STATE]
proof (state)
this:
infinite A

goal (3 subgoals):
 1. \<And>A. infinite A \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) A = zero
 2. aggregation.sum_0 (\<lambda>k. bot) {} = zero
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; aggregation.sum_0 (\<lambda>k. bot) F = zero\<rbrakk> \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
infinite A

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. bot) A = zero
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. bot) A = zero

goal (2 subgoals):
 1. aggregation.sum_0 (\<lambda>k. bot) {} = zero
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; aggregation.sum_0 (\<lambda>k. bot) F = zero\<rbrakk> \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. aggregation.sum_0 (\<lambda>k. bot) {} = zero
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; aggregation.sum_0 (\<lambda>k. bot) F = zero\<rbrakk> \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. aggregation.sum_0 (\<lambda>k. bot) {} = zero
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; aggregation.sum_0 (\<lambda>k. bot) F = zero\<rbrakk> \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. bot) {} = zero
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. bot) {} = zero

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; aggregation.sum_0 (\<lambda>k. bot) F = zero\<rbrakk> \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; aggregation.sum_0 (\<lambda>k. bot) F = zero\<rbrakk> \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
aggregation.sum_0 (\<lambda>k. bot) F = zero

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; aggregation.sum_0 (\<lambda>k. bot) F = zero\<rbrakk> \<Longrightarrow> aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
aggregation.sum_0 (\<lambda>k. bot) F = zero

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero
[PROOF STEP]
by (metis add.commute add_add_bot aggregation.sum_0.insert)
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. bot) (insert x F) = zero

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma agg_sum_bot_bot:
  "(\<Sum>\<^sub>k bot + bot::'a::aggregation_order) = bot + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. zero) {k. True} = zero
[PROOF STEP]
by (rule aggregation.sum_0.neutral_const)


[STATEMENT]
lemma agg_sum_not_bot_1:
  fixes f :: "'a::finite \<Rightarrow> 'b::aggregation_order"
  assumes "f i \<noteq> bot"
    shows "(\<Sum>\<^sub>k f k) \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 f {k. True} \<noteq> bot
[PROOF STEP]
by (metis assms add_bot aggregation.sum_0.remove finite_code mem_Collect_eq)


[STATEMENT]
lemma agg_sum_not_bot:
  fixes f :: "('a::finite,'b::aggregation_order) square"
  assumes "f (i,j) \<noteq> bot"
    shows "(\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l)) \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} \<noteq> bot
[PROOF STEP]
by (metis assms agg_sum_not_bot_1)


[STATEMENT]
lemma agg_sum_distrib:
  fixes f g :: "'a \<Rightarrow> 'b::aggregation_order"
  shows "(\<Sum>\<^sub>k f k + g k) = (\<Sum>\<^sub>k f k) + (\<Sum>\<^sub>k g k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + g k) {k. True} = aggregation.sum_0 f {k. True} + aggregation.sum_0 g {k. True}
[PROOF STEP]
by (rule aggregation.sum_0.distrib)


[STATEMENT]
lemma agg_sum_distrib_2:
  fixes f g :: "('a,'b::aggregation_order) square"
  shows "(\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l) + g (k,l)) = (\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l)) + (\<Sum>\<^sub>k \<Sum>\<^sub>l g (k,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
have "(\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l) + g (k,l)) = (\<Sum>\<^sub>k (\<Sum>\<^sub>l f (k,l)) + (\<Sum>\<^sub>l g (k,l)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True} + aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
by (metis (no_types) aggregation.sum_0.distrib)
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True} + aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True} + aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
have "... = (\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l)) + (\<Sum>\<^sub>k \<Sum>\<^sub>l g (k,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True} + aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
by (metis (no_types) aggregation.sum_0.distrib)
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True} + aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l) + g (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. g (k, l)) {l. True}) {k. True}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma agg_sum_add_bot:
  fixes f :: "'a \<Rightarrow> 'b::aggregation_order"
  shows "(\<Sum>\<^sub>k f k) = (\<Sum>\<^sub>k f k) + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 f {k. True} = aggregation.sum_0 f {k. True} + bot
[PROOF STEP]
by (metis (no_types) add_add_bot aggregation.sum_0.F_one)


[STATEMENT]
lemma agg_sum_add_bot_2:
  fixes f :: "'a \<Rightarrow> 'b::aggregation_order"
  shows "(\<Sum>\<^sub>k f k + bot) = (\<Sum>\<^sub>k f k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
have "(\<Sum>\<^sub>k f k + bot) = (\<Sum>\<^sub>k f k) + (\<Sum>\<^sub>k::'a bot::'b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True} + aggregation.sum_0 (\<lambda>k. bot) {k. True}
[PROOF STEP]
using agg_sum_distrib
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>k. ?f k + ?g k) {k. True} = aggregation.sum_0 ?f {k. True} + aggregation.sum_0 ?g {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True} + aggregation.sum_0 (\<lambda>k. bot) {k. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True} + aggregation.sum_0 (\<lambda>k. bot) {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True} + aggregation.sum_0 (\<lambda>k. bot) {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
have "... = (\<Sum>\<^sub>k f k) + (bot + bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 f {k. True} + aggregation.sum_0 (\<lambda>k. bot) {k. True} = aggregation.sum_0 f {k. True} + zero
[PROOF STEP]
by (metis agg_sum_bot)
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 f {k. True} + aggregation.sum_0 (\<lambda>k. bot) {k. True} = aggregation.sum_0 f {k. True} + zero

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 f {k. True} + aggregation.sum_0 (\<lambda>k. bot) {k. True} = aggregation.sum_0 f {k. True} + zero

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
have "... = (\<Sum>\<^sub>k f k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 f {k. True} + zero = aggregation.sum_0 f {k. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 f {k. True} + zero = aggregation.sum_0 f {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. f k + bot) {k. True} = aggregation.sum_0 f {k. True}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma agg_sum_commute:
  fixes f :: "('a,'b::aggregation_order) square"
  shows "(\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l)) = (\<Sum>\<^sub>l \<Sum>\<^sub>k f (k,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>l. aggregation.sum_0 (\<lambda>k. f (k, l)) {k. True}) {l. True}
[PROOF STEP]
by (rule aggregation.sum_0.swap)


[STATEMENT]
lemma agg_delta:
  fixes f :: "'a::finite \<Rightarrow> 'b::aggregation_order"
  shows "(\<Sum>\<^sub>l if l = j then f l else zero) = f j + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else zero) {l. True} = f j + bot
[PROOF STEP]
apply (subst aggregation.sum_0.delta)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {l. True}
 2. (if j \<in> {l. True} then f j + zero else zero) = f j + bot
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if j \<in> {l. True} then f j + zero else zero) = f j + bot
[PROOF STEP]
by (metis add.commute add.left_commute add_add_bot mem_Collect_eq)


[STATEMENT]
lemma agg_delta_1:
  fixes f :: "'a::finite \<Rightarrow> 'b::aggregation_order"
  shows "(\<Sum>\<^sub>l if l = j then f l else bot) = f j + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
let ?f = "(\<lambda>l . if l = j then f l else bot)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
let ?S = "{l::'a . True}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
proof (cases "j \<in> ?S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
 2. j \<notin> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
j \<notin> {l. True}

goal (2 subgoals):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
 2. j \<notin> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j \<notin> {l. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
j \<in> {l. True}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
let ?A = "?S - {j}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
let ?B = "{j}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
j \<in> {l. True}
[PROOF STEP]
have eq: "?S = ?A \<union> ?B"
[PROOF STATE]
proof (prove)
using this:
j \<in> {l. True}

goal (1 subgoal):
 1. {l. True} = {l. True} - {j} \<union> {j}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{l. True} = {l. True} - {j} \<union> {j}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
have dj: "?A \<inter> ?B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({l. True} - {j}) \<inter> {j} = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
({l. True} - {j}) \<inter> {j} = {}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
have fAB: "finite ?A" "finite ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({l. True} - {j}) &&& finite {j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({l. True} - {j})
finite {j}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
have "aggregation.sum_0 ?f ?S = aggregation.sum_0 ?f ?A + aggregation.sum_0 ?f ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}
[PROOF STEP]
using aggregation.sum_0.union_disjoint[OF fAB dj, of ?f, unfolded eq [symmetric]]
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
have "... = aggregation.sum_0 (\<lambda>l . bot) ?A + aggregation.sum_0 ?f ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = aggregation.sum_0 (\<lambda>l. bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}
[PROOF STEP]
by (subst aggregation.sum_0.cong[where ?B="?A"]) simp_all
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = aggregation.sum_0 (\<lambda>l. bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = aggregation.sum_0 (\<lambda>l. bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
have "... = zero + aggregation.sum_0 ?f ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = zero + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}
[PROOF STEP]
by (metis (no_types, lifting) add.commute add_add_bot aggregation.sum_0.F_g_one aggregation.sum_0.neutral)
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = zero + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. bot) ({l. True} - {j}) + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = zero + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j}

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
have "... = zero + (f j + zero)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = zero + (f j + zero)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
zero + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = zero + (f j + zero)

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
zero + aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {j} = zero + (f j + zero)

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
have "... = f j + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero + (f j + zero) = f j + bot
[PROOF STEP]
by (metis add.commute add.left_commute add_add_bot)
[PROOF STATE]
proof (state)
this:
zero + (f j + zero) = f j + bot

goal (1 subgoal):
 1. j \<in> {l. True} \<Longrightarrow> aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if l = j then f l else bot) {l. True} = f j + bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma agg_delta_2:
  fixes f :: "('a::finite,'b::aggregation_order) square"
  shows "(\<Sum>\<^sub>k \<Sum>\<^sub>l if k = i \<and> l = j then f (k,l) else bot) = f (i,j) + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot
[PROOF STEP]
have "\<forall>k . (\<Sum>\<^sub>l if k = i \<and> l = j then f (k,l) else bot) = (if k = i then f (k,j) + bot else zero)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)
[PROOF STEP]
have "(\<Sum>\<^sub>l if k = i \<and> l = j then f (k,l) else bot) = (\<Sum>\<^sub>l if l = j then if k = i then f (k,l) else bot else bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = aggregation.sum_0 (\<lambda>l. if l = j then if k = i then f (k, l) else bot else bot) {l. True}
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = aggregation.sum_0 (\<lambda>l. if l = j then if k = i then f (k, l) else bot else bot) {l. True}

goal (1 subgoal):
 1. \<And>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = aggregation.sum_0 (\<lambda>l. if l = j then if k = i then f (k, l) else bot else bot) {l. True}

goal (1 subgoal):
 1. \<And>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)
[PROOF STEP]
have "... = (if k = i then f (k,j) else bot) + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if l = j then if k = i then f (k, l) else bot else bot) {l. True} = (if k = i then f (k, j) else bot) + bot
[PROOF STEP]
by (rule agg_delta_1)
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if l = j then if k = i then f (k, l) else bot else bot) {l. True} = (if k = i then f (k, j) else bot) + bot

goal (1 subgoal):
 1. \<And>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) else bot) + bot
[PROOF STEP]
show "(\<Sum>\<^sub>l if k = i \<and> l = j then f (k,l) else bot) = (if k = i then f (k,j) + bot else zero)"
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) else bot) + bot

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot
[PROOF STEP]
hence "(\<Sum>\<^sub>k \<Sum>\<^sub>l if k = i \<and> l = j then f (k,l) else bot) = (\<Sum>\<^sub>k if k = i then f (k,j) + bot else zero)"
[PROOF STATE]
proof (prove)
using this:
\<forall>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. if k = i then f (k, j) + bot else zero) {k. True}
[PROOF STEP]
using aggregation.sum_0.cong
[PROOF STATE]
proof (prove)
using this:
\<forall>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True} = (if k = i then f (k, j) + bot else zero)
\<lbrakk>?A = ?B; \<And>x. x \<in> ?B \<Longrightarrow> ?g x = ?h x\<rbrakk> \<Longrightarrow> aggregation.sum_0 ?g ?A = aggregation.sum_0 ?h ?B

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. if k = i then f (k, j) + bot else zero) {k. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. if k = i then f (k, j) + bot else zero) {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = aggregation.sum_0 (\<lambda>k. if k = i then f (k, j) + bot else zero) {k. True}

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot
[PROOF STEP]
have "... = f (i,j) + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. if k = i then f (k, j) + bot else zero) {k. True} = f (i, j) + bot
[PROOF STEP]
apply (subst agg_delta)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (i, j) + bot + bot = f (i, j) + bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. if k = i then f (k, j) + bot else zero) {k. True} = f (i, j) + bot

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. if k = i \<and> l = j then f (k, l) else bot) {l. True}) {k. True} = f (i, j) + bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bot_plus_bot:
  "mbot \<oplus>\<^sub>M mbot = mzero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mbot \<oplus>\<^sub>M mbot = mzero
[PROOF STEP]
by (simp add: plus_matrix_def bot_matrix_def zero_matrix_def)


[STATEMENT]
lemma sum_bot:
  "sum\<^sub>M (mbot :: ('a::enum,'b::aggregation_order) square) = mzero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum\<^sub>M mbot = mzero
[PROOF STEP]
proof (rule ext, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M mbot) (a, b) = mzero (a, b)
[PROOF STEP]
fix i j :: "'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M mbot) (a, b) = mzero (a, b)
[PROOF STEP]
have "(sum\<^sub>M mbot :: ('a,'b) square) (i,j) = (if i = hd enum_class.enum \<and> j = i then \<Sum>\<^sub>(k::'a) \<Sum>\<^sub>(l::'a) bot else bot + bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum\<^sub>M mbot) (i, j) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} else zero)
[PROOF STEP]
by (unfold sum_matrix_def bot_matrix_def) simp
[PROOF STATE]
proof (state)
this:
(sum\<^sub>M mbot) (i, j) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} else zero)

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M mbot) (a, b) = mzero (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(sum\<^sub>M mbot) (i, j) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} else zero)

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M mbot) (a, b) = mzero (a, b)
[PROOF STEP]
have "... = bot + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} else zero) = zero
[PROOF STEP]
using agg_sum_bot aggregation.sum_0.neutral
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>k. bot) {k. True} = zero
\<forall>x\<in>?A. ?g x = zero \<Longrightarrow> aggregation.sum_0 ?g ?A = zero

goal (1 subgoal):
 1. (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} else zero) = zero
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} else zero) = zero

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M mbot) (a, b) = mzero (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} else zero) = zero

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M mbot) (a, b) = mzero (a, b)
[PROOF STEP]
have "... = mzero (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero = mzero (i, j)
[PROOF STEP]
by (simp add: zero_matrix_def)
[PROOF STATE]
proof (state)
this:
zero = mzero (i, j)

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M mbot) (a, b) = mzero (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(sum\<^sub>M mbot) (i, j) = mzero (i, j)
[PROOF STEP]
show "(sum\<^sub>M mbot :: ('a,'b) square) (i,j) = mzero (i,j)"
[PROOF STATE]
proof (prove)
using this:
(sum\<^sub>M mbot) (i, j) = mzero (i, j)

goal (1 subgoal):
 1. (sum\<^sub>M mbot) (i, j) = mzero (i, j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(sum\<^sub>M mbot) (i, j) = mzero (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_plus_bot:
  fixes f :: "('a::enum,'b::aggregation_order) square"
  shows "sum\<^sub>M f \<oplus>\<^sub>M mbot = sum\<^sub>M f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum\<^sub>M f \<oplus>\<^sub>M mbot = sum\<^sub>M f
[PROOF STEP]
proof (rule ext, rule prod_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (a, b) = (sum\<^sub>M f) (a, b)
[PROOF STEP]
let ?h = "hd enum_class.enum"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (a, b) = (sum\<^sub>M f) (a, b)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (a, b) = (sum\<^sub>M f) (a, b)
[PROOF STEP]
have "(sum\<^sub>M f \<oplus>\<^sub>M mbot) (i,j) = (if i = ?h \<and> j = i then (\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l)) + bot else zero + bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (i, j) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot else zero + bot)
[PROOF STEP]
by (simp add: plus_matrix_def bot_matrix_def sum_matrix_def)
[PROOF STATE]
proof (state)
this:
(sum\<^sub>M f \<oplus>\<^sub>M mbot) (i, j) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot else zero + bot)

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (a, b) = (sum\<^sub>M f) (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(sum\<^sub>M f \<oplus>\<^sub>M mbot) (i, j) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot else zero + bot)

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (a, b) = (sum\<^sub>M f) (a, b)
[PROOF STEP]
have "... = (if i = ?h \<and> j = i then \<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l) else zero)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot else zero + bot) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} else zero)
[PROOF STEP]
by (metis (no_types, lifting) add_add_bot aggregation.sum_0.F_one)
[PROOF STATE]
proof (state)
this:
(if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot else zero + bot) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} else zero)

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (a, b) = (sum\<^sub>M f) (a, b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot else zero + bot) = (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} else zero)

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (a, b) = (sum\<^sub>M f) (a, b)
[PROOF STEP]
have "... = (sum\<^sub>M f) (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} else zero) = (sum\<^sub>M f) (i, j)
[PROOF STEP]
by (simp add: sum_matrix_def)
[PROOF STATE]
proof (state)
this:
(if i = hd enum_class.enum \<and> j = i then aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} else zero) = (sum\<^sub>M f) (i, j)

goal (1 subgoal):
 1. \<And>x a b. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (a, b) = (sum\<^sub>M f) (a, b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(sum\<^sub>M f \<oplus>\<^sub>M mbot) (i, j) = (sum\<^sub>M f) (i, j)
[PROOF STEP]
show "(sum\<^sub>M f \<oplus>\<^sub>M mbot) (i,j) = (sum\<^sub>M f) (i,j)"
[PROOF STATE]
proof (prove)
using this:
(sum\<^sub>M f \<oplus>\<^sub>M mbot) (i, j) = (sum\<^sub>M f) (i, j)

goal (1 subgoal):
 1. (sum\<^sub>M f \<oplus>\<^sub>M mbot) (i, j) = (sum\<^sub>M f) (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(sum\<^sub>M f \<oplus>\<^sub>M mbot) (i, j) = (sum\<^sub>M f) (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_plus_zero:
  fixes f :: "('a::enum,'b::aggregation_order) square"
  shows "sum\<^sub>M f \<oplus>\<^sub>M mzero = sum\<^sub>M f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum\<^sub>M f \<oplus>\<^sub>M mzero = sum\<^sub>M f
[PROOF STEP]
by (rule ext, rule prod_cases) (simp add: plus_matrix_def zero_matrix_def sum_matrix_def)


[STATEMENT]
lemma agg_matrix_bot:
  fixes f :: "('a,'b::aggregation_order) square"
  assumes "\<forall>i j . f (i,j) = bot"
    shows "f = mbot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = mbot
[PROOF STEP]
apply (unfold bot_matrix_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = (\<lambda>e. bot)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i j. f (i, j) = bot

goal (1 subgoal):
 1. f = (\<lambda>e. bot)
[PROOF STEP]
by auto


[STATEMENT]
lemma sum_bot_2:
  "sum2\<^sub>M (mbot :: ('a,'b::aggregation_order) square) = mzero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum2\<^sub>M mbot = mzero
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M mbot) x = mzero x
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M mbot) x = mzero x
[PROOF STEP]
have "(sum2\<^sub>M mbot :: ('a,'b) square) e = (\<Sum>\<^sub>(k::'a) \<Sum>\<^sub>(l::'a) bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum2\<^sub>M mbot) e = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True}
[PROOF STEP]
by (unfold sum_matrix_2_def bot_matrix_def) simp
[PROOF STATE]
proof (state)
this:
(sum2\<^sub>M mbot) e = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True}

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M mbot) x = mzero x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(sum2\<^sub>M mbot) e = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True}

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M mbot) x = mzero x
[PROOF STEP]
have "... = bot + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} = zero
[PROOF STEP]
using agg_sum_bot aggregation.sum_0.neutral
[PROOF STATE]
proof (prove)
using this:
aggregation.sum_0 (\<lambda>k. bot) {k. True} = zero
\<forall>x\<in>?A. ?g x = zero \<Longrightarrow> aggregation.sum_0 ?g ?A = zero

goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} = zero
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} = zero

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M mbot) x = mzero x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. bot) {l. True}) {k. True} = zero

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M mbot) x = mzero x
[PROOF STEP]
have "... = mzero e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero = mzero e
[PROOF STEP]
by (simp add: zero_matrix_def)
[PROOF STATE]
proof (state)
this:
zero = mzero e

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M mbot) x = mzero x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(sum2\<^sub>M mbot) e = mzero e
[PROOF STEP]
show "(sum2\<^sub>M mbot :: ('a,'b) square) e = mzero e"
[PROOF STATE]
proof (prove)
using this:
(sum2\<^sub>M mbot) e = mzero e

goal (1 subgoal):
 1. (sum2\<^sub>M mbot) e = mzero e
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(sum2\<^sub>M mbot) e = mzero e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_plus_bot_2:
  fixes f :: "('a,'b::aggregation_order) square"
  shows "sum2\<^sub>M f \<oplus>\<^sub>M mbot = sum2\<^sub>M f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum2\<^sub>M f \<oplus>\<^sub>M mbot = sum2\<^sub>M f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) x = (sum2\<^sub>M f) x
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) x = (sum2\<^sub>M f) x
[PROOF STEP]
have "(sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = (\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l)) + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot
[PROOF STEP]
by (simp add: plus_matrix_def bot_matrix_def sum_matrix_2_def)
[PROOF STATE]
proof (state)
this:
(sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) x = (sum2\<^sub>M f) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) x = (sum2\<^sub>M f) x
[PROOF STEP]
have "... = (\<Sum>\<^sub>k \<Sum>\<^sub>l f (k,l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True}
[PROOF STEP]
by (metis (no_types, lifting) add_add_bot aggregation.sum_0.F_one)
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True}

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) x = (sum2\<^sub>M f) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} + bot = aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True}

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) x = (sum2\<^sub>M f) x
[PROOF STEP]
have "... = (sum2\<^sub>M f) e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} = (sum2\<^sub>M f) e
[PROOF STEP]
by (simp add: sum_matrix_2_def)
[PROOF STATE]
proof (state)
this:
aggregation.sum_0 (\<lambda>k. aggregation.sum_0 (\<lambda>l. f (k, l)) {l. True}) {k. True} = (sum2\<^sub>M f) e

goal (1 subgoal):
 1. \<And>x. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) x = (sum2\<^sub>M f) x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = (sum2\<^sub>M f) e
[PROOF STEP]
show "(sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = (sum2\<^sub>M f) e"
[PROOF STATE]
proof (prove)
using this:
(sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = (sum2\<^sub>M f) e

goal (1 subgoal):
 1. (sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = (sum2\<^sub>M f) e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(sum2\<^sub>M f \<oplus>\<^sub>M mbot) e = (sum2\<^sub>M f) e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_plus_zero_2:
  fixes f :: "('a,'b::aggregation_order) square"
  shows "sum2\<^sub>M f \<oplus>\<^sub>M mzero = sum2\<^sub>M f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum2\<^sub>M f \<oplus>\<^sub>M mzero = sum2\<^sub>M f
[PROOF STEP]
by (simp add: plus_matrix_def zero_matrix_def sum_matrix_2_def)


[STATEMENT]
lemma enum_pos'_inverse:
  "List.member xs x \<Longrightarrow> xs!(enum_pos' xs x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List.member xs x \<Longrightarrow> xs ! enum_pos' xs x = x
[PROOF STEP]
apply (induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. List.member [] x \<Longrightarrow> [] ! enum_pos' [] x = x
 2. \<And>a xs. \<lbrakk>List.member xs x \<Longrightarrow> xs ! enum_pos' xs x = x; List.member (a # xs) x\<rbrakk> \<Longrightarrow> (a # xs) ! enum_pos' (a # xs) x = x
[PROOF STEP]
apply (simp add: member_rec(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>List.member xs x \<Longrightarrow> xs ! enum_pos' xs x = x; List.member (a # xs) x\<rbrakk> \<Longrightarrow> (a # xs) ! enum_pos' (a # xs) x = x
[PROOF STEP]
by (metis diff_add_inverse enum_pos'.simps(2) less_one member_rec(1) not_add_less1 nth_Cons')


[STATEMENT]
lemma enum_pos_inverse [simp]:
  "enum_class.enum!(enum_pos x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum_class.enum ! enum_pos x = x
[PROOF STEP]
apply (unfold enum_pos.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum_class.enum ! enum_pos' enum_class.enum x = x
[PROOF STEP]
apply (rule enum_pos'_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List.member enum_class.enum x
[PROOF STEP]
by (metis in_enum List.member_def)


[STATEMENT]
lemma enum_pos_injective [simp]:
  "enum_pos x = enum_pos y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum_pos x = enum_pos y \<Longrightarrow> x = y
[PROOF STEP]
by (metis enum_pos_inverse)


[STATEMENT]
lemma minarc_at_most_one:
  fixes f :: "('a::enum,'b::{aggregation_order,top}) square"
  assumes "(minarc\<^sub>M f) e \<noteq> bot"
      and "(minarc\<^sub>M f) d \<noteq> bot"
    shows "e = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e = d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. e = d
[PROOF STEP]
have 1: "f e + bot \<le> f d + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f e + bot \<le> f d + bot
[PROOF STEP]
by (metis assms minarc_matrix_def)
[PROOF STATE]
proof (state)
this:
f e + bot \<le> f d + bot

goal (1 subgoal):
 1. e = d
[PROOF STEP]
have "f d + bot \<le> f e + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f d + bot \<le> f e + bot
[PROOF STEP]
by (metis assms minarc_matrix_def)
[PROOF STATE]
proof (state)
this:
f d + bot \<le> f e + bot

goal (1 subgoal):
 1. e = d
[PROOF STEP]
hence "f e + bot = f d + bot"
[PROOF STATE]
proof (prove)
using this:
f d + bot \<le> f e + bot

goal (1 subgoal):
 1. f e + bot = f d + bot
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
f d + bot \<le> f e + bot
f e + bot \<le> f d + bot

goal (1 subgoal):
 1. f e + bot = f d + bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f e + bot = f d + bot

goal (1 subgoal):
 1. e = d
[PROOF STEP]
hence "\<not> enum_lex_less d e \<and> \<not> enum_lex_less e d"
[PROOF STATE]
proof (prove)
using this:
f e + bot = f d + bot

goal (1 subgoal):
 1. \<not> enum_lex_less d e \<and> \<not> enum_lex_less e d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f e + bot = f d + bot
(minarc\<^sub>M f) e \<noteq> bot
(minarc\<^sub>M f) d \<noteq> bot

goal (1 subgoal):
 1. \<not> enum_lex_less d e \<and> \<not> enum_lex_less e d
[PROOF STEP]
by (unfold minarc_matrix_def) (metis (lifting))
[PROOF STATE]
proof (state)
this:
\<not> enum_lex_less d e \<and> \<not> enum_lex_less e d

goal (1 subgoal):
 1. e = d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> enum_lex_less d e \<and> \<not> enum_lex_less e d

goal (1 subgoal):
 1. e = d
[PROOF STEP]
using enum_pos_injective less_linear
[PROOF STATE]
proof (prove)
using this:
\<not> enum_lex_less d e \<and> \<not> enum_lex_less e d
enum_pos ?x = enum_pos ?y \<Longrightarrow> ?x = ?y
?x < ?y \<or> ?x = ?y \<or> ?y < ?x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma least_order:
  assumes transitive: "\<forall>x y z . le x y \<and> le y z \<longrightarrow> le x z"
      and total: "\<forall>x y . le x y \<or> le y x"
    shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<exists>x . x \<in> A \<and> (\<forall>y . y \<in> A \<longrightarrow> le x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> (\<forall>y. y \<in> A \<longrightarrow> le x y)
[PROOF STEP]
proof (induct A rule: finite_ne_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<exists>xa. xa \<in> {x} \<and> (\<forall>y. y \<in> {x} \<longrightarrow> le xa y)
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<exists>x. x \<in> F \<and> (\<forall>y. y \<in> F \<longrightarrow> le x y)\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> insert x F \<and> (\<forall>y. y \<in> insert x F \<longrightarrow> le xa y)
[PROOF STEP]
case singleton
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. \<exists>xa. xa \<in> {x} \<and> (\<forall>y. y \<in> {x} \<longrightarrow> le xa y)
 2. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<exists>x. x \<in> F \<and> (\<forall>y. y \<in> F \<longrightarrow> le x y)\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> insert x F \<and> (\<forall>y. y \<in> insert x F \<longrightarrow> le xa y)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xa. xa \<in> {x_} \<and> (\<forall>y. y \<in> {x_} \<longrightarrow> le xa y)
[PROOF STEP]
using total
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. le x y \<or> le y x

goal (1 subgoal):
 1. \<exists>xa. xa \<in> {x_} \<and> (\<forall>y. y \<in> {x_} \<longrightarrow> le xa y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xa. xa \<in> {x_} \<and> (\<forall>y. y \<in> {x_} \<longrightarrow> le xa y)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<exists>x. x \<in> F \<and> (\<forall>y. y \<in> F \<longrightarrow> le x y)\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> insert x F \<and> (\<forall>y. y \<in> insert x F \<longrightarrow> le xa y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<exists>x. x \<in> F \<and> (\<forall>y. y \<in> F \<longrightarrow> le x y)\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> insert x F \<and> (\<forall>y. y \<in> insert x F \<longrightarrow> le xa y)
[PROOF STEP]
case insert
[PROOF STATE]
proof (state)
this:
finite F_
F_ \<noteq> {}
x_ \<notin> F_
\<exists>x. x \<in> F_ \<and> (\<forall>y. y \<in> F_ \<longrightarrow> le x y)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; F \<noteq> {}; x \<notin> F; \<exists>x. x \<in> F \<and> (\<forall>y. y \<in> F \<longrightarrow> le x y)\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> insert x F \<and> (\<forall>y. y \<in> insert x F \<longrightarrow> le xa y)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite F_
F_ \<noteq> {}
x_ \<notin> F_
\<exists>x. x \<in> F_ \<and> (\<forall>y. y \<in> F_ \<longrightarrow> le x y)

goal (1 subgoal):
 1. \<exists>xa. xa \<in> insert x_ F_ \<and> (\<forall>y. y \<in> insert x_ F_ \<longrightarrow> le xa y)
[PROOF STEP]
by (metis insert_iff transitive total)
[PROOF STATE]
proof (state)
this:
\<exists>xa. xa \<in> insert x_ F_ \<and> (\<forall>y. y \<in> insert x_ F_ \<longrightarrow> le xa y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma minarc_at_least_one:
  fixes f :: "('a::enum,'b::linear_aggregation_lattice) square"
  assumes "f \<noteq> mbot"
    shows "\<exists>e . (minarc\<^sub>M f) e = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
let ?nbe = "{ (e,f e) | e . f e \<noteq> bot }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 1: "finite ?nbe"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(e, f e) |e. f e \<noteq> bot}
[PROOF STEP]
using finite_code finite_image_set
[PROOF STATE]
proof (prove)
using this:
finite ?A = True
finite {x. ?P x} \<Longrightarrow> finite {?f x |x. ?P x}

goal (1 subgoal):
 1. finite {(e, f e) |e. f e \<noteq> bot}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite {(e, f e) |e. f e \<noteq> bot}

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 2: "?nbe \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(e, f e) |e. f e \<noteq> bot} \<noteq> {}
[PROOF STEP]
using assms agg_matrix_bot
[PROOF STATE]
proof (prove)
using this:
f \<noteq> mbot
\<forall>i j. ?f (i, j) = bot \<Longrightarrow> ?f = mbot

goal (1 subgoal):
 1. {(e, f e) |e. f e \<noteq> bot} \<noteq> {}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{(e, f e) |e. f e \<noteq> bot} \<noteq> {}

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
let ?le = "\<lambda>(e::'a \<times> 'a,fe::'b) (d::'a \<times> 'a,fd) . fe + bot \<le> fd + bot"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 3: "\<forall>x y z . ?le x y \<and> ?le y z \<longrightarrow> ?le x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y z. (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y \<and> (case y of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) z \<longrightarrow> (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x y z. (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y \<and> (case y of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) z \<longrightarrow> (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) z

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 4: "\<forall>x y . ?le x y \<or> ?le y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y \<or> (case y of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) x
[PROOF STEP]
by (simp add: linear)
[PROOF STATE]
proof (state)
this:
\<forall>x y. (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y \<or> (case y of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) x

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have "\<exists>x . x \<in> ?nbe \<and> (\<forall>y . y \<in> ?nbe \<longrightarrow> ?le x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y)
[PROOF STEP]
by (rule least_order, rule 3, rule 4, rule 1, rule 2)
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y)

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y)
[PROOF STEP]
obtain e fe where 5: "(e,fe) \<in> ?nbe \<and> (\<forall>y . y \<in> ?nbe \<longrightarrow> ?le (e,fe) y)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case x of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y)

goal (1 subgoal):
 1. (\<And>e fe. (e, fe) \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case (e, fe) of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(e, fe) \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case (e, fe) of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y)

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
let ?me = "{ e . f e \<noteq> bot \<and> f e + bot = fe + bot }"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 6: "finite ?me"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {e. f e \<noteq> bot \<and> f e + bot = fe + bot}
[PROOF STEP]
using finite_code finite_image_set
[PROOF STATE]
proof (prove)
using this:
finite ?A = True
finite {x. ?P x} \<Longrightarrow> finite {?f x |x. ?P x}

goal (1 subgoal):
 1. finite {e. f e \<noteq> bot \<and> f e + bot = fe + bot}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite {e. f e \<noteq> bot \<and> f e + bot = fe + bot}

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 7: "?me \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<noteq> {}
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
(e, fe) \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case (e, fe) of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y)

goal (1 subgoal):
 1. {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<noteq> {}

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 8: "\<forall>x y z . enum_lex_less_eq x y \<and> enum_lex_less_eq y z \<longrightarrow> enum_lex_less_eq x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y z. enum_lex_less_eq x y \<and> enum_lex_less_eq y z \<longrightarrow> enum_lex_less_eq x z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x y z. enum_lex_less_eq x y \<and> enum_lex_less_eq y z \<longrightarrow> enum_lex_less_eq x z

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 9: "\<forall>x y . enum_lex_less_eq x y \<or> enum_lex_less_eq y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. enum_lex_less_eq x y \<or> enum_lex_less_eq y x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x y. enum_lex_less_eq x y \<or> enum_lex_less_eq y x

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have "\<exists>x . x \<in> ?me \<and> (\<forall>y . y \<in> ?me \<longrightarrow> enum_lex_less_eq x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. x \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq x y)
[PROOF STEP]
by (rule least_order, rule 8, rule 9, rule 6, rule 7)
[PROOF STATE]
proof (state)
this:
\<exists>x. x \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq x y)

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq x y)
[PROOF STEP]
obtain m where 10: "m \<in> ?me \<and> (\<forall>y . y \<in> ?me \<longrightarrow> enum_lex_less_eq m y)"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq x y)

goal (1 subgoal):
 1. (\<And>m. m \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq m y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq m y)

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 11: "f m \<noteq> bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f m \<noteq> bot
[PROOF STEP]
using 10 5
[PROOF STATE]
proof (prove)
using this:
m \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq m y)
(e, fe) \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case (e, fe) of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y)

goal (1 subgoal):
 1. f m \<noteq> bot
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f m \<noteq> bot

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have 12: "\<forall>d. f d \<noteq> bot \<longrightarrow> f m + bot \<le> f d + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d. f d \<noteq> bot \<longrightarrow> f m + bot \<le> f d + bot
[PROOF STEP]
using 10 5
[PROOF STATE]
proof (prove)
using this:
m \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq m y)
(e, fe) \<in> {(e, f e) |e. f e \<noteq> bot} \<and> (\<forall>y. y \<in> {(e, f e) |e. f e \<noteq> bot} \<longrightarrow> (case (e, fe) of (e, fe) \<Rightarrow> \<lambda>(d, fd). fe + bot \<le> fd + bot) y)

goal (1 subgoal):
 1. \<forall>d. f d \<noteq> bot \<longrightarrow> f m + bot \<le> f d + bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>d. f d \<noteq> bot \<longrightarrow> f m + bot \<le> f d + bot

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
have "\<forall>d. f d \<noteq> bot \<and> enum_lex_less d m \<longrightarrow> f m + bot \<noteq> f d + bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d. f d \<noteq> bot \<and> enum_lex_less d m \<longrightarrow> f m + bot \<noteq> f d + bot
[PROOF STEP]
using 10
[PROOF STATE]
proof (prove)
using this:
m \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<and> (\<forall>y. y \<in> {e. f e \<noteq> bot \<and> f e + bot = fe + bot} \<longrightarrow> enum_lex_less_eq m y)

goal (1 subgoal):
 1. \<forall>d. f d \<noteq> bot \<and> enum_lex_less d m \<longrightarrow> f m + bot \<noteq> f d + bot
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>d. f d \<noteq> bot \<and> enum_lex_less d m \<longrightarrow> f m + bot \<noteq> f d + bot

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
hence "(minarc\<^sub>M f) m = top"
[PROOF STATE]
proof (prove)
using this:
\<forall>d. f d \<noteq> bot \<and> enum_lex_less d m \<longrightarrow> f m + bot \<noteq> f d + bot

goal (1 subgoal):
 1. (minarc\<^sub>M f) m = top
[PROOF STEP]
using 11 12
[PROOF STATE]
proof (prove)
using this:
\<forall>d. f d \<noteq> bot \<and> enum_lex_less d m \<longrightarrow> f m + bot \<noteq> f d + bot
f m \<noteq> bot
\<forall>d. f d \<noteq> bot \<longrightarrow> f m + bot \<le> f d + bot

goal (1 subgoal):
 1. (minarc\<^sub>M f) m = top
[PROOF STEP]
by (simp add: minarc_matrix_def)
[PROOF STATE]
proof (state)
this:
(minarc\<^sub>M f) m = top

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(minarc\<^sub>M f) m = top

goal (1 subgoal):
 1. \<exists>e. (minarc\<^sub>M f) e = top
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>e. (minarc\<^sub>M f) e = top

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma regular_bot_top_2:
  "regular x \<longleftrightarrow> x = bot \<or> x = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular x = (x = bot \<or> x = top)
[PROOF STEP]
by simp


[STATEMENT]
lemma "x AND y = x OR (y :: uint16)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND y = x OR y
[PROOF STEP]
quickcheck[random, expect=counterexample]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND y = x OR y
[PROOF STEP]
quickcheck[exhaustive, expect=counterexample]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x AND y = x OR y
[PROOF STEP]
oops


[STATEMENT]
lemma in_progress_dom [elim]: "in_progress (r R) x \<Longrightarrow> R \<in> dom r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_progress (r R) x \<Longrightarrow> R \<in> dom r
[PROOF STEP]
by (cases "r R", auto)


[STATEMENT]
lemma in_progress_Some [elim]: "in_progress r x \<Longrightarrow> \<exists> x. r = Some x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_progress r x \<Longrightarrow> \<exists>x. r = Some x
[PROOF STEP]
by (cases "r", auto)


[STATEMENT]
lemma in_progressS_elt [elim]: "in_progressS r S \<Longrightarrow> x \<in> S \<Longrightarrow> in_progress r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_progressS r S; x \<in> S\<rbrakk> \<Longrightarrow> in_progress r x
[PROOF STEP]
by (cases r, auto)


[STATEMENT]
lemma comp_char [simp]:
    shows "g \<cdot>\<^sup>o\<^sup>p f = f \<cdot> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<cdot>\<^sup>o\<^sup>p f = f \<cdot> g
[PROOF STEP]
using comp_def
[PROOF STATE]
proof (prove)
using this:
?g \<cdot>\<^sup>o\<^sup>p ?f \<equiv> ?f \<cdot> ?g

goal (1 subgoal):
 1. g \<cdot>\<^sup>o\<^sup>p f = f \<cdot> g
[PROOF STEP]
by auto


[STATEMENT]
lemma null_char [simp]:
    shows "null = C.null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null = C.null
[PROOF STEP]
by (metis C.comp_null(2) comp_null(2) comp_def)


[STATEMENT]
lemma ide_char [simp]:
    shows "ide a \<longleftrightarrow> C.ide a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide a = C.ide a
[PROOF STEP]
unfolding ide_def C.ide_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<cdot>\<^sup>o\<^sup>p a \<noteq> null \<and> (\<forall>f. (f \<cdot>\<^sup>o\<^sup>p a \<noteq> null \<longrightarrow> f \<cdot>\<^sup>o\<^sup>p a = f) \<and> (a \<cdot>\<^sup>o\<^sup>p f \<noteq> null \<longrightarrow> a \<cdot>\<^sup>o\<^sup>p f = f))) = (a \<cdot> a \<noteq> C.null \<and> (\<forall>f. (f \<cdot> a \<noteq> C.null \<longrightarrow> f \<cdot> a = f) \<and> (a \<cdot> f \<noteq> C.null \<longrightarrow> a \<cdot> f = f)))
[PROOF STEP]
by auto


[STATEMENT]
lemma domains_char:
    shows "domains f = C.codomains f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domains f = C.codomains f
[PROOF STEP]
using C.codomains_def domains_def ide_char
[PROOF STATE]
proof (prove)
using this:
C.codomains ?f \<equiv> {b. C.ide b \<and> b \<cdot> ?f \<noteq> C.null}
domains ?f \<equiv> {a. ide a \<and> ?f \<cdot>\<^sup>o\<^sup>p a \<noteq> null}
ide ?a = C.ide ?a

goal (1 subgoal):
 1. domains f = C.codomains f
[PROOF STEP]
by auto


[STATEMENT]
lemma codomains_char:
    shows "codomains f = C.domains f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. codomains f = C.domains f
[PROOF STEP]
using C.domains_def codomains_def ide_char
[PROOF STATE]
proof (prove)
using this:
C.domains ?f \<equiv> {a. C.ide a \<and> ?f \<cdot> a \<noteq> C.null}
codomains ?f \<equiv> {b. ide b \<and> b \<cdot>\<^sup>o\<^sup>p ?f \<noteq> null}
ide ?a = C.ide ?a

goal (1 subgoal):
 1. codomains f = C.domains f
[PROOF STEP]
by auto


[STATEMENT]
lemma is_category:
    shows "category comp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category (\<cdot>\<^sup>o\<^sup>p)
[PROOF STEP]
..


[STATEMENT]
lemma dom_char [simp]:
    shows "dom f = C.cod f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom f = C.cod f
[PROOF STEP]
by (simp add: C.cod_def dom_def domains_char)


[STATEMENT]
lemma cod_char [simp]:
    shows "cod f = C.dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cod f = C.dom f
[PROOF STEP]
by (simp add: C.dom_def cod_def codomains_char)


[STATEMENT]
lemma arr_char [simp]:
    shows "arr f \<longleftrightarrow> C.arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr f = C.arr f
[PROOF STEP]
using C.has_codomain_iff_arr has_domain_iff_arr domains_char
[PROOF STATE]
proof (prove)
using this:
(C.codomains ?f \<noteq> {}) = C.arr ?f
(domains ?f \<noteq> {}) = arr ?f
domains ?f = C.codomains ?f

goal (1 subgoal):
 1. arr f = C.arr f
[PROOF STEP]
by auto


[STATEMENT]
lemma hom_char [simp]:
    shows "in_hom f b a \<longleftrightarrow> C.in_hom f a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f : b \<leftarrow> a\<guillemotright> = \<guillemotleft>f : a \<rightarrow> b\<guillemotright>
[PROOF STEP]
by force


[STATEMENT]
lemma seq_char [simp]:
    shows "seq g f = C.seq f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq g f = C.seq f g
[PROOF STEP]
by simp


[STATEMENT]
lemma soundness_diagonalize_JNF':
  fixes A::"'a mat"
  assumes "is_bezout_ext bezout" and "A \<in> carrier_mat m n"
  and "diagonalize_JNF A bezout = (P,S,Q)"
  shows "P \<in> carrier_mat m m \<and> Q \<in> carrier_mat n n \<and> S \<in> carrier_mat m n
      \<and> invertible_mat P \<and> invertible_mat Q \<and> isDiagonal_mat S \<and> S = P*A*Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> Q \<in> carrier_mat n n \<and> S \<in> carrier_mat m n \<and> invertible_mat P \<and> invertible_mat Q \<and> isDiagonal_mat S \<and> S = P * A * Q
[PROOF STEP]
using soundness_diagonalize_JNF assms
[PROOF STATE]
proof (prove)
using this:
\<forall>A bezout. A \<in> carrier_mat ?m ?n \<and> is_bezout_ext bezout \<longrightarrow> (case diagonalize_JNF A bezout of (P, S, Q) \<Rightarrow> P \<in> carrier_mat ?m ?m \<and> Q \<in> carrier_mat ?n ?n \<and> S \<in> carrier_mat ?m ?n \<and> invertible_mat P \<and> invertible_mat Q \<and> isDiagonal_mat S \<and> S = P * A * Q)
is_bezout_ext bezout
A \<in> carrier_mat m n
diagonalize_JNF A bezout = (P, S, Q)

goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> Q \<in> carrier_mat n n \<and> S \<in> carrier_mat m n \<and> invertible_mat P \<and> invertible_mat Q \<and> isDiagonal_mat S \<and> S = P * A * Q
[PROOF STEP]
unfolding case_prod_beta
[PROOF STATE]
proof (prove)
using this:
\<forall>A bezout. A \<in> carrier_mat ?m ?n \<and> is_bezout_ext bezout \<longrightarrow> fst (diagonalize_JNF A bezout) \<in> carrier_mat ?m ?m \<and> snd (snd (diagonalize_JNF A bezout)) \<in> carrier_mat ?n ?n \<and> fst (snd (diagonalize_JNF A bezout)) \<in> carrier_mat ?m ?n \<and> invertible_mat (fst (diagonalize_JNF A bezout)) \<and> invertible_mat (snd (snd (diagonalize_JNF A bezout))) \<and> isDiagonal_mat (fst (snd (diagonalize_JNF A bezout))) \<and> fst (snd (diagonalize_JNF A bezout)) = fst (diagonalize_JNF A bezout) * A * snd (snd (diagonalize_JNF A bezout))
is_bezout_ext bezout
A \<in> carrier_mat m n
diagonalize_JNF A bezout = (P, S, Q)

goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> Q \<in> carrier_mat n n \<and> S \<in> carrier_mat m n \<and> invertible_mat P \<and> invertible_mat Q \<and> isDiagonal_mat S \<and> S = P * A * Q
[PROOF STEP]
by (metis fst_conv snd_conv)


[STATEMENT]
lemma soundness_diagonalize:
  assumes b: "is_bezout_ext bezout"
  and d: "diagonalize A bezout = (P,S,Q)"
shows "invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P**A**Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
define A' where "A' = Mod_Type_Connect.from_hma\<^sub>m A"
[PROOF STATE]
proof (state)
this:
A' = Mod_Type_Connect.from_hma\<^sub>m A

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
obtain P' S' Q' where d_JNF: "(P',S',Q') = diagonalize_JNF A' bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P' S' Q'. (P', S', Q') = diagonalize_JNF A' bezout \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
(P', S', Q') = diagonalize_JNF A' bezout

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
define m and n where "m = dim_row A'" and "n = dim_col A'"
[PROOF STATE]
proof (state)
this:
m = dim_row A'
n = dim_col A'

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
hence A': "A' \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
using this:
m = dim_row A'
n = dim_col A'

goal (1 subgoal):
 1. A' \<in> carrier_mat m n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' \<in> carrier_mat m n

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have res_JNF: "P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n
      \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P'*A'*Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'
[PROOF STEP]
by (rule soundness_diagonalize_JNF'[OF b A' d_JNF[symmetric]])
[PROOF STATE]
proof (state)
this:
P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have "Mod_Type_Connect.to_hma\<^sub>m P' = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m P' = P
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
local.diagonalize A bezout = (P, S, Q)

goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m P' = P
[PROOF STEP]
unfolding diagonalize_def Let_def
[PROOF STATE]
proof (prove)
using this:
(case diagonalize_JNF (Mod_Type_Connect.from_hma\<^sub>m A) bezout of (P, S, Q) \<Rightarrow> (Mod_Type_Connect.to_hma\<^sub>m P, Mod_Type_Connect.to_hma\<^sub>m S, Mod_Type_Connect.to_hma\<^sub>m Q)) = (P, S, Q)

goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m P' = P
[PROOF STEP]
by (metis A'_def d_JNF fst_conv old.prod.case)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.to_hma\<^sub>m P' = P

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
hence "P' = Mod_Type_Connect.from_hma\<^sub>m P"
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.to_hma\<^sub>m P' = P

goal (1 subgoal):
 1. P' = Mod_Type_Connect.from_hma\<^sub>m P
[PROOF STEP]
using A'_def m_def res_JNF
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.to_hma\<^sub>m P' = P
A' = Mod_Type_Connect.from_hma\<^sub>m A
m = dim_row A'
P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'

goal (1 subgoal):
 1. P' = Mod_Type_Connect.from_hma\<^sub>m P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P' = Mod_Type_Connect.from_hma\<^sub>m P

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
hence [transfer_rule]: "Mod_Type_Connect.HMA_M P' P"
[PROOF STATE]
proof (prove)
using this:
P' = Mod_Type_Connect.from_hma\<^sub>m P

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M P' P
[PROOF STEP]
unfolding Mod_Type_Connect.HMA_M_def
[PROOF STATE]
proof (prove)
using this:
P' = Mod_Type_Connect.from_hma\<^sub>m P

goal (1 subgoal):
 1. P' = Mod_Type_Connect.from_hma\<^sub>m P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M P' P

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have "Mod_Type_Connect.to_hma\<^sub>m Q' = Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m Q' = Q
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
local.diagonalize A bezout = (P, S, Q)

goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m Q' = Q
[PROOF STEP]
unfolding diagonalize_def Let_def
[PROOF STATE]
proof (prove)
using this:
(case diagonalize_JNF (Mod_Type_Connect.from_hma\<^sub>m A) bezout of (P, S, Q) \<Rightarrow> (Mod_Type_Connect.to_hma\<^sub>m P, Mod_Type_Connect.to_hma\<^sub>m S, Mod_Type_Connect.to_hma\<^sub>m Q)) = (P, S, Q)

goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m Q' = Q
[PROOF STEP]
by (metis A'_def d_JNF snd_conv old.prod.case)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.to_hma\<^sub>m Q' = Q

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
hence "Q' = Mod_Type_Connect.from_hma\<^sub>m Q"
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.to_hma\<^sub>m Q' = Q

goal (1 subgoal):
 1. Q' = Mod_Type_Connect.from_hma\<^sub>m Q
[PROOF STEP]
using A'_def n_def res_JNF
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.to_hma\<^sub>m Q' = Q
A' = Mod_Type_Connect.from_hma\<^sub>m A
n = dim_col A'
P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'

goal (1 subgoal):
 1. Q' = Mod_Type_Connect.from_hma\<^sub>m Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q' = Mod_Type_Connect.from_hma\<^sub>m Q

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
hence [transfer_rule]: "Mod_Type_Connect.HMA_M Q' Q"
[PROOF STATE]
proof (prove)
using this:
Q' = Mod_Type_Connect.from_hma\<^sub>m Q

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M Q' Q
[PROOF STEP]
unfolding Mod_Type_Connect.HMA_M_def
[PROOF STATE]
proof (prove)
using this:
Q' = Mod_Type_Connect.from_hma\<^sub>m Q

goal (1 subgoal):
 1. Q' = Mod_Type_Connect.from_hma\<^sub>m Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M Q' Q

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have "Mod_Type_Connect.to_hma\<^sub>m S' = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m S' = S
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
local.diagonalize A bezout = (P, S, Q)

goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m S' = S
[PROOF STEP]
unfolding diagonalize_def Let_def
[PROOF STATE]
proof (prove)
using this:
(case diagonalize_JNF (Mod_Type_Connect.from_hma\<^sub>m A) bezout of (P, S, Q) \<Rightarrow> (Mod_Type_Connect.to_hma\<^sub>m P, Mod_Type_Connect.to_hma\<^sub>m S, Mod_Type_Connect.to_hma\<^sub>m Q)) = (P, S, Q)

goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m S' = S
[PROOF STEP]
by (metis A'_def d_JNF snd_conv old.prod.case)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.to_hma\<^sub>m S' = S

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
hence "S' = Mod_Type_Connect.from_hma\<^sub>m S"
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.to_hma\<^sub>m S' = S

goal (1 subgoal):
 1. S' = Mod_Type_Connect.from_hma\<^sub>m S
[PROOF STEP]
using A'_def m_def n_def res_JNF
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.to_hma\<^sub>m S' = S
A' = Mod_Type_Connect.from_hma\<^sub>m A
m = dim_row A'
n = dim_col A'
P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'

goal (1 subgoal):
 1. S' = Mod_Type_Connect.from_hma\<^sub>m S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S' = Mod_Type_Connect.from_hma\<^sub>m S

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
hence [transfer_rule]: "Mod_Type_Connect.HMA_M S' S"
[PROOF STATE]
proof (prove)
using this:
S' = Mod_Type_Connect.from_hma\<^sub>m S

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M S' S
[PROOF STEP]
unfolding Mod_Type_Connect.HMA_M_def
[PROOF STATE]
proof (prove)
using this:
S' = Mod_Type_Connect.from_hma\<^sub>m S

goal (1 subgoal):
 1. S' = Mod_Type_Connect.from_hma\<^sub>m S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M S' S

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_M A' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M A' A
[PROOF STEP]
using A'_def
[PROOF STATE]
proof (prove)
using this:
A' = Mod_Type_Connect.from_hma\<^sub>m A

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M A' A
[PROOF STEP]
unfolding Mod_Type_Connect.HMA_M_def
[PROOF STATE]
proof (prove)
using this:
A' = Mod_Type_Connect.from_hma\<^sub>m A

goal (1 subgoal):
 1. A' = Mod_Type_Connect.from_hma\<^sub>m A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M A' A

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have "invertible P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible P
[PROOF STEP]
using res_JNF
[PROOF STATE]
proof (prove)
using this:
P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'

goal (1 subgoal):
 1. invertible P
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
invertible P

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
invertible P

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have "invertible Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible Q
[PROOF STEP]
using res_JNF
[PROOF STATE]
proof (prove)
using this:
P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'

goal (1 subgoal):
 1. invertible Q
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
invertible Q

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
invertible Q

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have "isDiagonal S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isDiagonal S
[PROOF STEP]
using res_JNF
[PROOF STATE]
proof (prove)
using this:
P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'

goal (1 subgoal):
 1. isDiagonal S
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
isDiagonal S

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isDiagonal S

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
have "S = P**A**Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = P ** A ** Q
[PROOF STEP]
using res_JNF
[PROOF STATE]
proof (prove)
using this:
P' \<in> carrier_mat m m \<and> Q' \<in> carrier_mat n n \<and> S' \<in> carrier_mat m n \<and> invertible_mat P' \<and> invertible_mat Q' \<and> isDiagonal_mat S' \<and> S' = P' * A' * Q'

goal (1 subgoal):
 1. S = P ** A ** Q
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
S = P ** A ** Q

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
invertible P
invertible Q
isDiagonal S
S = P ** A ** Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invertible P
invertible Q
isDiagonal S
S = P ** A ** Q

goal (1 subgoal):
 1. invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
invertible P \<and> invertible Q \<and> isDiagonal S \<and> S = P ** A ** Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DA_delta_is_lift_NA_delta:
 "\<And>Q. DA.delta (na2da A) w Q = Union(NA.delta A w ` Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Q. DA.delta (na2da A) w Q = \<Union> (NA.delta A w ` Q)
[PROOF STEP]
by (induct w)(auto simp:na2da_def)


[STATEMENT]
lemma NA_DA_equiv:
  "NA.accepts A w = DA.accepts (na2da A) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NA.accepts A w = DA.accepts (na2da A) w
[PROOF STEP]
apply (simp add: DA.accepts_def NA.accepts_def DA_delta_is_lift_NA_delta)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>q\<in>NA.delta A w (start A). fin A q) = fin (na2da A) (\<Union> (NA.delta A w ` start (na2da A)))
[PROOF STEP]
apply (simp add: na2da_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma espclosure_DA_delta_is_steps:
 "\<And>Q. (eps A)\<^sup>* `` (DA.delta (nae2da A) w Q) = steps A w `` Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Q. (eps A)\<^sup>* `` DA.delta (nae2da A) w Q = NAe.steps A w `` Q
[PROOF STEP]
apply (induct w)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Q. (eps A)\<^sup>* `` DA.delta (nae2da A) [] Q = NAe.steps A [] `` Q
 2. \<And>a w Q. (\<And>Q. (eps A)\<^sup>* `` DA.delta (nae2da A) w Q = NAe.steps A w `` Q) \<Longrightarrow> (eps A)\<^sup>* `` DA.delta (nae2da A) (a # w) Q = NAe.steps A (a # w) `` Q
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a w Q. (\<And>Q. (eps A)\<^sup>* `` DA.delta (nae2da A) w Q = NAe.steps A w `` Q) \<Longrightarrow> (eps A)\<^sup>* `` DA.delta (nae2da A) (a # w) Q = NAe.steps A (a # w) `` Q
[PROOF STEP]
apply (simp add: step_def nae2da_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a w Q. (\<And>Q. {(p, q). q \<in> next A None p}\<^sup>* `` DA.delta ({start A}, \<lambda>a Q. \<Union> (next A (Some a) ` {(p, q). q \<in> next A None p}\<^sup>* `` Q), \<lambda>Q. \<exists>p\<in>{(p, q). q \<in> next A None p}\<^sup>* `` Q. fin A p) w Q = NAe.steps A w `` Q) \<Longrightarrow> NAe.steps A w `` \<Union> (next A (Some a) ` {(p, q). q \<in> next A None p}\<^sup>* `` Q) = ({(p, q). q \<in> next A None p}\<^sup>* O {(p, q). q \<in> next A (Some a) p} O NAe.steps A w) `` Q
[PROOF STEP]
apply (blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma NAe_DA_equiv:
  "DA.accepts (nae2da A) w = NAe.accepts A w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DA.accepts (nae2da A) w = NAe.accepts A w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. DA.accepts (nae2da A) w = NAe.accepts A w
[PROOF STEP]
have "\<And>Q. fin (nae2da A) Q = (\<exists>q \<in> (eps A)\<^sup>* `` Q. fin A q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Q. fin (nae2da A) Q = (\<exists>q\<in>(eps A)\<^sup>* `` Q. fin A q)
[PROOF STEP]
by(simp add:nae2da_def)
[PROOF STATE]
proof (state)
this:
fin (nae2da A) ?Q = (\<exists>q\<in>(eps A)\<^sup>* `` ?Q. fin A q)

goal (1 subgoal):
 1. DA.accepts (nae2da A) w = NAe.accepts A w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fin (nae2da A) ?Q = (\<exists>q\<in>(eps A)\<^sup>* `` ?Q. fin A q)

goal (1 subgoal):
 1. DA.accepts (nae2da A) w = NAe.accepts A w
[PROOF STEP]
apply(simp add:espclosure_DA_delta_is_steps NAe.accepts_def DA.accepts_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q. fin (nae2da A) Q = (\<exists>q\<in>(eps A)\<^sup>* `` Q. fin A q)) \<Longrightarrow> (\<exists>x\<in>NAe.steps A w `` start (nae2da A). fin A x) = (\<exists>q. (start A, q) \<in> NAe.steps A w \<and> fin A q)
[PROOF STEP]
apply(simp add:nae2da_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>NAe.steps A w `` {start A}. fin A x) = (\<exists>q. (start A, q) \<in> NAe.steps A w \<and> fin A q)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
DA.accepts (nae2da A) w = NAe.accepts A w

goal:
No subgoals!
[PROOF STEP]
qed