[STATEMENT]
lemma zoom_comp1: "l1 \<rhd> l2 \<rhd> s = (l2 ;\<^sub>L l1) \<rhd> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l1 \<rhd> l2 \<rhd> s = (l2 ;\<^sub>L l1) \<rhd> s
[PROOF STEP]
unfolding zoom_def lens_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State (\<lambda>b. case run_state (State (\<lambda>b. case run_state s (get\<^bsub>l2\<^esub> b) of (c, a) \<Rightarrow> (c, put\<^bsub>l2\<^esub> b a))) (get\<^bsub>l1\<^esub> b) of (c, a) \<Rightarrow> (c, put\<^bsub>l1\<^esub> b a)) = State (\<lambda>b. case run_state s (get\<^bsub>\<lparr>lens_get = get\<^bsub>l2\<^esub> \<circ> get\<^bsub>l1\<^esub>, lens_put = \<lambda>\<sigma> v. put\<^bsub>l1\<^esub> \<sigma> (put\<^bsub>l2\<^esub> (get\<^bsub>l1\<^esub> \<sigma>) v)\<rparr>\<^esub> b) of (c, a) \<Rightarrow> (c, put\<^bsub>\<lparr>lens_get = get\<^bsub>l2\<^esub> \<circ> get\<^bsub>l1\<^esub>, lens_put = \<lambda>\<sigma> v. put\<^bsub>l1\<^esub> \<sigma> (put\<^bsub>l2\<^esub> (get\<^bsub>l1\<^esub> \<sigma>) v)\<rparr>\<^esub> b a))
[PROOF STEP]
by (auto split: prod.splits)


[STATEMENT]
lemma zoom_zero[simp]: "zero_lens \<rhd> s = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>L \<rhd> s = s
[PROOF STEP]
unfolding zoom_def zero_lens_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State (\<lambda>b. case run_state s (get\<^bsub>\<lparr>lens_get = \<lambda>_. (), lens_put = \<lambda>\<sigma> x. \<sigma>\<rparr>\<^esub> b) of (c, a) \<Rightarrow> (c, put\<^bsub>\<lparr>lens_get = \<lambda>_. (), lens_put = \<lambda>\<sigma> x. \<sigma>\<rparr>\<^esub> b a)) = s
[PROOF STEP]
by simp


[STATEMENT]
lemma zoom_id[simp]: "id_lens \<rhd> s = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sub>L \<rhd> s = s
[PROOF STEP]
unfolding zoom_def id_lens_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State (\<lambda>b. case run_state s (get\<^bsub>\<lparr>lens_get = id, lens_put = \<lambda>_. id\<rparr>\<^esub> b) of (c, a) \<Rightarrow> (c, put\<^bsub>\<lparr>lens_get = id, lens_put = \<lambda>_. id\<rparr>\<^esub> b a)) = s
[PROOF STEP]
by simp


[STATEMENT]
lemma (in mwb_lens) zoom_comp2[simp]: "zoom x m \<bind> (\<lambda>a. zoom x (n a)) = zoom x (m \<bind> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zoom x m \<bind> (\<lambda>a. zoom x (n a)) = zoom x (m \<bind> n)
[PROOF STEP]
unfolding zoom_def State_Monad.bind_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State (\<lambda>s. case run_state (State (\<lambda>b. case run_state m (get b) of (c, a) \<Rightarrow> (c, put b a))) s of (a, xa) \<Rightarrow> run_state (State (\<lambda>b. case run_state (n a) (get b) of (c, a) \<Rightarrow> (c, put b a))) xa) = State (\<lambda>b. case run_state (State (\<lambda>s. case run_state m s of (a, x) \<Rightarrow> run_state (n a) x)) (get b) of (c, a) \<Rightarrow> (c, put b a))
[PROOF STEP]
by (auto split: prod.splits simp: put_get put_put)


[STATEMENT]
lemma (in wb_lens) use_alt_def: "use x = map_state (lens_get x) State_Monad.get"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. use x = map_state get State_Monad.get
[PROOF STEP]
unfolding State_Monad.get_def use_def zoom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State (\<lambda>b. case run_state (State (\<lambda>s. (s, s))) (get b) of (c, a) \<Rightarrow> (c, put b a)) = map_state get (State (\<lambda>s. (s, s)))
[PROOF STEP]
by (simp add: comp_def get_put)


[STATEMENT]
lemma (in wb_lens) modify_alt_def: "modify x f = State_Monad.update (update f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. modify x f = State_Monad.update (update f)
[PROOF STEP]
unfolding modify_def zoom_def lens_update_def State_Monad.update_def State_Monad.get_def State_Monad.set_def State_Monad.bind_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State (\<lambda>b. case run_state (State (\<lambda>s. case run_state (State (\<lambda>s. (s, s))) s of (a, x) \<Rightarrow> run_state (((\<lambda>s'. State (\<lambda>_. ((), s'))) \<circ> f) a) x)) (get b) of (c, a) \<Rightarrow> (c, put b a)) = State (\<lambda>s. case run_state (State (\<lambda>s. (s, s))) s of (a, xa) \<Rightarrow> run_state (((\<lambda>s'. State (\<lambda>_. ((), s'))) \<circ> (\<lambda>\<sigma>. put \<sigma> (f (get \<sigma>)))) a) xa)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma (in wb_lens) modify_id[simp]: "modify x (\<lambda>x. x) = State_Monad.return ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. modify x (\<lambda>x. x) = State_Monad.return ()
[PROOF STEP]
unfolding lens_update_def modify_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. State_Monad.update (\<lambda>\<sigma>. put \<sigma> (get \<sigma>)) = State_Monad.return ()
[PROOF STEP]
by (simp add: get_put)


[STATEMENT]
lemma (in mwb_lens) modify_comp[simp]: "bind (modify x f) (\<lambda>_. modify x g) = modify x (g \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. modify x f \<bind> (\<lambda>_. modify x g) = modify x (g \<circ> f)
[PROOF STEP]
unfolding modify_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zoom x (State_Monad.update f) \<bind> (\<lambda>_. zoom x (State_Monad.update g)) = zoom x (State_Monad.update (g \<circ> f))
[PROOF STEP]
by simp


[STATEMENT]
lemma HMA_submatrix[transfer_rule]: "(HMA_M ===> HMA_M) (\<lambda>A. submatrix A I J)
  ((\<lambda>A. submatrix_hma A I J):: 'a^ 'nc ^ 'nr \<Rightarrow> 'a ^ 'nc2 ^ 'nr2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (HMA_M ===> HMA_M) (\<lambda>A. submatrix A I J) (\<lambda>A. submatrix_hma A I J)
[PROOF STEP]
proof (intro rel_funI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. HMA_M x y \<Longrightarrow> HMA_M (submatrix x I J) (submatrix_hma y I J)
[PROOF STEP]
case (1 A B)
[PROOF STATE]
proof (state)
this:
HMA_M A B

goal (1 subgoal):
 1. \<And>x y. HMA_M x y \<Longrightarrow> HMA_M (submatrix x I J) (submatrix_hma y I J)
[PROOF STEP]
note relAB[transfer_rule] = this
[PROOF STATE]
proof (state)
this:
HMA_M A B

goal (1 subgoal):
 1. \<And>x y. HMA_M x y \<Longrightarrow> HMA_M (submatrix x I J) (submatrix_hma y I J)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M (submatrix A I J) (submatrix_hma B I J)
[PROOF STEP]
unfolding  HMA_M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A I J = from_hma\<^sub>m (submatrix_hma B I J)
[PROOF STEP]
proof (rule eq_matI, auto)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
 2. dim_row (submatrix A I J) = CARD('nr2)
 3. dim_col (submatrix A I J) = CARD('nc2)
[PROOF STEP]
show "dim_row (submatrix A I J) = CARD('nr2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (submatrix A I J) = CARD('nr2)
[PROOF STEP]
unfolding submatrix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (Matrix.mat (card {i. i < dim_row A \<and> i \<in> I}) (card {j. j < dim_col A \<and> j \<in> J}) (\<lambda>(i, j). A $$ (pick I i, pick J j))) = CARD('nr2)
[PROOF STEP]
using I dim_row_transfer_rule relAB
[PROOF STATE]
proof (prove)
using this:
card {i. i < CARD('nr) \<and> i \<in> I} = CARD('nr2)
HMA_M ?A ?A' \<Longrightarrow> dim_row ?A = CARD(?'nr)
HMA_M A B

goal (1 subgoal):
 1. dim_row (Matrix.mat (card {i. i < dim_row A \<and> i \<in> I}) (card {j. j < dim_col A \<and> j \<in> J}) (\<lambda>(i, j). A $$ (pick I i, pick J j))) = CARD('nr2)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
dim_row (submatrix A I J) = CARD('nr2)

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
 2. dim_col (submatrix A I J) = CARD('nc2)
[PROOF STEP]
show "dim_col (submatrix A I J) = CARD('nc2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (submatrix A I J) = CARD('nc2)
[PROOF STEP]
unfolding submatrix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (Matrix.mat (card {i. i < dim_row A \<and> i \<in> I}) (card {j. j < dim_col A \<and> j \<in> J}) (\<lambda>(i, j). A $$ (pick I i, pick J j))) = CARD('nc2)
[PROOF STEP]
using J dim_col_transfer_rule relAB
[PROOF STATE]
proof (prove)
using this:
card {i. i < CARD('nc) \<and> i \<in> J} = CARD('nc2)
HMA_M ?A ?A' \<Longrightarrow> dim_col ?A = CARD(?'nc)
HMA_M A B

goal (1 subgoal):
 1. dim_col (Matrix.mat (card {i. i < dim_row A \<and> i \<in> I}) (card {j. j < dim_col A \<and> j \<in> J}) (\<lambda>(i, j). A $$ (pick I i, pick J j))) = CARD('nc2)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
dim_col (submatrix A I J) = CARD('nc2)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
let ?B="(submatrix_hma B I J)::'a ^ 'nc2 ^ 'nr2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
assume i: "i < CARD('nr2)" and
           j: "j < CARD('nc2)"
[PROOF STATE]
proof (state)
this:
i < CARD('nr2)
j < CARD('nc2)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have i2: "i < card {i. i < dim_row A \<and> i \<in> I}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < card {i. i < dim_row A \<and> i \<in> I}
[PROOF STEP]
using I dim_row_transfer_rule i relAB
[PROOF STATE]
proof (prove)
using this:
card {i. i < CARD('nr) \<and> i \<in> I} = CARD('nr2)
HMA_M ?A ?A' \<Longrightarrow> dim_row ?A = CARD(?'nr)
i < CARD('nr2)
HMA_M A B

goal (1 subgoal):
 1. i < card {i. i < dim_row A \<and> i \<in> I}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
i < card {i. i < dim_row A \<and> i \<in> I}

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have j2: "j < card {j. j < dim_col A \<and> j \<in> J}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < card {j. j < dim_col A \<and> j \<in> J}
[PROOF STEP]
using J dim_col_transfer_rule j relAB
[PROOF STATE]
proof (prove)
using this:
card {i. i < CARD('nc) \<and> i \<in> J} = CARD('nc2)
HMA_M ?A ?A' \<Longrightarrow> dim_col ?A = CARD(?'nc)
j < CARD('nc2)
HMA_M A B

goal (1 subgoal):
 1. j < card {j. j < dim_col A \<and> j \<in> J}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
j < card {j. j < dim_col A \<and> j \<in> J}

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
let ?i = "(from_nat (pick I i))::'nr"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
let ?j = "(from_nat (pick J j))::'nc"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
let ?i' = "Bij_Nat.to_nat ((Bij_Nat.from_nat i)::'nr2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
let ?j' = "Bij_Nat.to_nat ((Bij_Nat.from_nat j)::'nc2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have i': "?i' = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bij_Nat.to_nat (Bij_Nat.from_nat i) = i
[PROOF STEP]
by (rule to_nat_from_nat_id[OF i])
[PROOF STATE]
proof (state)
this:
Bij_Nat.to_nat (Bij_Nat.from_nat i) = i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have j': "?j' = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bij_Nat.to_nat (Bij_Nat.from_nat j) = j
[PROOF STEP]
by (rule to_nat_from_nat_id[OF j])
[PROOF STATE]
proof (state)
this:
Bij_Nat.to_nat (Bij_Nat.from_nat j) = j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
let ?f = "(\<lambda>(i, j).
         B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat ((Bij_Nat.from_nat i)::'nr2))) $h
         Bij_Nat.from_nat (pick J (Bij_Nat.to_nat ((Bij_Nat.from_nat j)::'nc2))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have [transfer_rule]: "HMA_I (pick I i) ?i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_I (pick I i) (Bij_Nat.from_nat (pick I i))
[PROOF STEP]
by (simp add: Bij_Nat.to_nat_from_nat_id I i pick_le HMA_I_def)
[PROOF STATE]
proof (state)
this:
HMA_I (pick I i) (Bij_Nat.from_nat (pick I i))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have [transfer_rule]: "HMA_I (pick J j) ?j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_I (pick J j) (Bij_Nat.from_nat (pick J j))
[PROOF STEP]
by (simp add: Bij_Nat.to_nat_from_nat_id J j pick_le HMA_I_def)
[PROOF STATE]
proof (state)
this:
HMA_I (pick J j) (Bij_Nat.from_nat (pick J j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have "submatrix A I J $$ (i, j) = A $$ (pick I i, pick J j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submatrix A I J $$ (i, j) = A $$ (pick I i, pick J j)
[PROOF STEP]
by (rule submatrix_index[OF i2 j2])
[PROOF STATE]
proof (state)
this:
submatrix A I J $$ (i, j) = A $$ (pick I i, pick J j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
submatrix A I J $$ (i, j) = A $$ (pick I i, pick J j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have "... = index_hma B ?i ?j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (pick I i, pick J j) = index_hma B (Bij_Nat.from_nat (pick I i)) (Bij_Nat.from_nat (pick J j))
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
A $$ (pick I i, pick J j) = index_hma B (Bij_Nat.from_nat (pick I i)) (Bij_Nat.from_nat (pick J j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $$ (pick I i, pick J j) = index_hma B (Bij_Nat.from_nat (pick I i)) (Bij_Nat.from_nat (pick J j))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have "... =  B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat ((Bij_Nat.from_nat i)::'nr2))) $h
         Bij_Nat.from_nat (pick J (Bij_Nat.to_nat ((Bij_Nat.from_nat j)::'nc2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index_hma B (Bij_Nat.from_nat (pick I i)) (Bij_Nat.from_nat (pick J j)) = B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))
[PROOF STEP]
unfolding i' j' index_hma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B $h Bij_Nat.from_nat (pick I i) $h Bij_Nat.from_nat (pick J j) = B $h Bij_Nat.from_nat (pick I i) $h Bij_Nat.from_nat (pick J j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index_hma B (Bij_Nat.from_nat (pick I i)) (Bij_Nat.from_nat (pick J j)) = B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
index_hma B (Bij_Nat.from_nat (pick I i)) (Bij_Nat.from_nat (pick J j)) = B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have "... = ?f (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j))) = (case (i, j) of (i, j) \<Rightarrow> B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j))) = (case (i, j) of (i, j) \<Rightarrow> B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j))))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j))) = (case (i, j) of (i, j) \<Rightarrow> B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j))))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have "... = Matrix.mat CARD('nr2) CARD('nc2) ?f $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (i, j) of (i, j) \<Rightarrow> B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) = Matrix.mat CARD('nr2) CARD('nc2) (\<lambda>(i, j). B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) $$ (i, j)
[PROOF STEP]
by (rule index_mat[symmetric, OF i j])
[PROOF STATE]
proof (state)
this:
(case (i, j) of (i, j) \<Rightarrow> B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) = Matrix.mat CARD('nr2) CARD('nc2) (\<lambda>(i, j). B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(case (i, j) of (i, j) \<Rightarrow> B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) = Matrix.mat CARD('nr2) CARD('nc2) (\<lambda>(i, j). B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
have "... = from_hma\<^sub>m ?B $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.mat CARD('nr2) CARD('nc2) (\<lambda>(i, j). B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
unfolding from_hma\<^sub>m_def submatrix_hma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.mat CARD('nr2) CARD('nc2) (\<lambda>(i, j). B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) $$ (i, j) = Matrix.mat CARD('nr2) CARD('nc2) (\<lambda>(i, j). (\<chi>a b. B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat a)) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat b))) $h Bij_Nat.from_nat i $h Bij_Nat.from_nat j) $$ (i, j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Matrix.mat CARD('nr2) CARD('nc2) (\<lambda>(i, j). B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat (Bij_Nat.from_nat i))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat (Bij_Nat.from_nat j)))) $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < CARD('nr2); j < CARD('nc2)\<rbrakk> \<Longrightarrow> submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
show "submatrix A I J $$ (i, j) = from_hma\<^sub>m ?B $$ (i, j)"
[PROOF STATE]
proof (prove)
using this:
submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)

goal (1 subgoal):
 1. submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
submatrix A I J $$ (i, j) = from_hma\<^sub>m (submatrix_hma B I J) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
HMA_M (submatrix A I J) (submatrix_hma B I J)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Cauchy_Binet_HOL_Analysis:
  fixes A::"'a::comm_ring_1^'m^'n" and B::"'a^'n^'m"
  shows "Determinants.det (A**B) = (\<Sum>I\<in>{I. I\<subseteq>{0..<ncols A} \<and> card I=nrows A}.
         Determinants.det ((submatrix_hma A UNIV I)::'a^'n^'n) *
         Determinants.det ((submatrix_hma B I UNIV)::'a^'n^'n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
let ?A = "(from_hma\<^sub>m A)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
let ?B = "(from_hma\<^sub>m B)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
have relA[transfer_rule]: "HMA_M ?A A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M (from_hma\<^sub>m A) A
[PROOF STEP]
unfolding HMA_M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_hma\<^sub>m A = from_hma\<^sub>m A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
HMA_M (from_hma\<^sub>m A) A

goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
have relB[transfer_rule]: "HMA_M ?B B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M (from_hma\<^sub>m B) B
[PROOF STEP]
unfolding HMA_M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. from_hma\<^sub>m B = from_hma\<^sub>m B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
HMA_M (from_hma\<^sub>m B) B

goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
have "(\<Sum>I\<in>{I. I\<subseteq>{0..<ncols A} \<and> card I = nrows A}.
         Determinants.det ((submatrix_hma A UNIV I)::'a^'n^'n) *
         Determinants.det ((submatrix_hma B I UNIV)::'a^'n^'n)) =
          (\<Sum>I\<in>{I. I\<subseteq>{0..<ncols A} \<and> card I=nrows A}. det (submatrix ?A UNIV I)
        * det (submatrix ?B I UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV)) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinant.det (submatrix (from_hma\<^sub>m A) UNIV I) * Determinant.det (submatrix (from_hma\<^sub>m B) I UNIV))
[PROOF STEP]
proof (rule sum.cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
fix I
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
assume I: "I \<in>{I. I\<subseteq>{0..<ncols A} \<and> card I=nrows A}"
[PROOF STATE]
proof (state)
this:
I \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}

goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
let ?sub_A= "((submatrix_hma A UNIV I)::'a^'n^'n)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
let ?sub_B= "((submatrix_hma B I UNIV)::'a^'n^'n)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
have c1: "card {i. i < CARD('n) \<and> i \<in> UNIV} = CARD('n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. i < CARD('n) \<and> i \<in> UNIV} = CARD('n)
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
I \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}

goal (1 subgoal):
 1. card {i. i < CARD('n) \<and> i \<in> UNIV} = CARD('n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {i. i < CARD('n) \<and> i \<in> UNIV} = CARD('n)

goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
have c2: "card {i. i < CARD('m) \<and> i \<in> I} = CARD('n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. i < CARD('m) \<and> i \<in> I} = CARD('n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {i. i < CARD('m) \<and> i \<in> I} = CARD('n)
[PROOF STEP]
have "I = {i. i < CARD('m) \<and> i \<in> I}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I = {i. i < CARD('m) \<and> i \<in> I}
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
I \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}

goal (1 subgoal):
 1. I = {i. i < CARD('m) \<and> i \<in> I}
[PROOF STEP]
unfolding nrows_def ncols_def
[PROOF STATE]
proof (prove)
using this:
I \<in> {I. I \<subseteq> {0..<CARD('m)} \<and> card I = CARD('n)}

goal (1 subgoal):
 1. I = {i. i < CARD('m) \<and> i \<in> I}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I = {i. i < CARD('m) \<and> i \<in> I}

goal (1 subgoal):
 1. card {i. i < CARD('m) \<and> i \<in> I} = CARD('n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
I = {i. i < CARD('m) \<and> i \<in> I}

goal (1 subgoal):
 1. card {i. i < CARD('m) \<and> i \<in> I} = CARD('n)
[PROOF STEP]
using I nrows_def
[PROOF STATE]
proof (prove)
using this:
I = {i. i < CARD('m) \<and> i \<in> I}
I \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
nrows ?A = CARD(?'rows)

goal (1 subgoal):
 1. card {i. i < CARD('m) \<and> i \<in> I} = CARD('n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {i. i < CARD('m) \<and> i \<in> I} = CARD('n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {i. i < CARD('m) \<and> i \<in> I} = CARD('n)

goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
have [transfer_rule]: "HMA_M (submatrix ?A UNIV I) ?sub_A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M (submatrix (from_hma\<^sub>m A) UNIV I) (submatrix_hma A UNIV I)
[PROOF STEP]
using HMA_submatrix[OF c1 c2] relA
[PROOF STATE]
proof (prove)
using this:
rel_fun HMA_M HMA_M (\<lambda>A. submatrix A UNIV I) (\<lambda>A. submatrix_hma A UNIV I)
HMA_M (from_hma\<^sub>m A) A

goal (1 subgoal):
 1. HMA_M (submatrix (from_hma\<^sub>m A) UNIV I) (submatrix_hma A UNIV I)
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. HMA_M x y \<longrightarrow> HMA_M (submatrix x UNIV I) (submatrix_hma y UNIV I)
HMA_M (from_hma\<^sub>m A) A

goal (1 subgoal):
 1. HMA_M (submatrix (from_hma\<^sub>m A) UNIV I) (submatrix_hma A UNIV I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_M (submatrix (from_hma\<^sub>m A) UNIV I) (submatrix_hma A UNIV I)

goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
have [transfer_rule]: "HMA_M (submatrix ?B I UNIV) ?sub_B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M (submatrix (from_hma\<^sub>m B) I UNIV) (submatrix_hma B I UNIV)
[PROOF STEP]
using HMA_submatrix[OF c2 c1] relB
[PROOF STATE]
proof (prove)
using this:
rel_fun HMA_M HMA_M (\<lambda>A. submatrix A I UNIV) (\<lambda>A. submatrix_hma A I UNIV)
HMA_M (from_hma\<^sub>m B) B

goal (1 subgoal):
 1. HMA_M (submatrix (from_hma\<^sub>m B) I UNIV) (submatrix_hma B I UNIV)
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. HMA_M x y \<longrightarrow> HMA_M (submatrix x I UNIV) (submatrix_hma y I UNIV)
HMA_M (from_hma\<^sub>m B) B

goal (1 subgoal):
 1. HMA_M (submatrix (from_hma\<^sub>m B) I UNIV) (submatrix_hma B I UNIV)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_M (submatrix (from_hma\<^sub>m B) I UNIV) (submatrix_hma B I UNIV)

goal (2 subgoals):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
 2. \<And>x. x \<in> {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} \<Longrightarrow> Determinants.det (submatrix_hma A UNIV x) * Determinants.det (submatrix_hma B x UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV x) * Determinant.det (submatrix (from_hma\<^sub>m B) x UNIV)
[PROOF STEP]
show "Determinants.det ?sub_A * Determinants.det ?sub_B
      = det (submatrix ?A UNIV I) * det (submatrix ?B I UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV I) * Determinant.det (submatrix (from_hma\<^sub>m B) I UNIV)
[PROOF STEP]
by (transfer', auto)
[PROOF STATE]
proof (state)
this:
Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV) = Determinant.det (submatrix (from_hma\<^sub>m A) UNIV I) * Determinant.det (submatrix (from_hma\<^sub>m B) I UNIV)

goal (1 subgoal):
 1. {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A} = {I. I \<subseteq> {0..<ncols A} \<and> card I = nrows A}
[PROOF STEP]
qed (auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV)) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinant.det (submatrix (from_hma\<^sub>m A) UNIV I) * Determinant.det (submatrix (from_hma\<^sub>m B) I UNIV))

goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV)) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinant.det (submatrix (from_hma\<^sub>m A) UNIV I) * Determinant.det (submatrix (from_hma\<^sub>m B) I UNIV))

goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
have "... = det (?A*?B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinant.det (submatrix (from_hma\<^sub>m A) UNIV I) * Determinant.det (submatrix (from_hma\<^sub>m B) I UNIV)) = Determinant.det (from_hma\<^sub>m A * from_hma\<^sub>m B)
[PROOF STEP]
by (rule Cauchy_Binet[symmetric], unfold nrows_def ncols_def, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinant.det (submatrix (from_hma\<^sub>m A) UNIV I) * Determinant.det (submatrix (from_hma\<^sub>m B) I UNIV)) = Determinant.det (from_hma\<^sub>m A * from_hma\<^sub>m B)

goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinant.det (submatrix (from_hma\<^sub>m A) UNIV I) * Determinant.det (submatrix (from_hma\<^sub>m B) I UNIV)) = Determinant.det (from_hma\<^sub>m A * from_hma\<^sub>m B)

goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
have "... = Determinants.det (A**B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Determinant.det (from_hma\<^sub>m A * from_hma\<^sub>m B) = Determinants.det (A ** B)
[PROOF STEP]
by (transfer', auto)
[PROOF STATE]
proof (state)
this:
Determinant.det (from_hma\<^sub>m A * from_hma\<^sub>m B) = Determinants.det (A ** B)

goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV)) = Determinants.det (A ** B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV)) = Determinants.det (A ** B)

goal (1 subgoal):
 1. Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Determinants.det (A ** B) = (\<Sum>I | I \<subseteq> {0..<ncols A} \<and> card I = nrows A. Determinants.det (submatrix_hma A UNIV I) * Determinants.det (submatrix_hma B I UNIV))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ap_stream_id: "pure (\<lambda>x. x) \<diamondop> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure (\<lambda>x. x) \<diamondop> x = x
[PROOF STEP]
by (coinduction arbitrary: x) simp


[STATEMENT]
lemma ap_stream_homo: "pure f \<diamondop> pure x = pure (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure f \<diamondop> pure x = pure (f x)
[PROOF STEP]
by coinduction simp


[STATEMENT]
lemma ap_stream_interchange: "f \<diamondop> pure x = pure (\<lambda>f. f x) \<diamondop> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<diamondop> pure x = pure (\<lambda>f. f x) \<diamondop> f
[PROOF STEP]
by (coinduction arbitrary: f) auto


[STATEMENT]
lemma ap_stream_composition: "pure (\<lambda>g f x. g (f x)) \<diamondop> g \<diamondop> f \<diamondop> x = g \<diamondop> (f \<diamondop> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure (\<lambda>g f x. g (f x)) \<diamondop> g \<diamondop> f \<diamondop> x = g \<diamondop> (f \<diamondop> x)
[PROOF STEP]
by (coinduction arbitrary: g f x) auto


[STATEMENT]
lemma smap_applicative[applicative_unfold]: "smap f x = pure f \<diamondop> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap f x = pure f \<diamondop> x
[PROOF STEP]
unfolding ap_stream_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap f x = corec_stream (\<lambda>(f, x). shd f (shd x)) (\<lambda>(f, x). False) (\<lambda>(f, x). undefined) (\<lambda>(f, x). (stl f, stl x)) (pure f, x)
[PROOF STEP]
by (coinduction arbitrary: x) auto


[STATEMENT]
lemma smap2_applicative[applicative_unfold]: "smap2 f x y = pure f \<diamondop> x \<diamondop> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap2 f x y = pure f \<diamondop> x \<diamondop> y
[PROOF STEP]
unfolding ap_stream_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap2 f x y = corec_stream (\<lambda>(f, x). shd f (shd x)) (\<lambda>(f, x). False) (\<lambda>(f, x). undefined) (\<lambda>(f, x). (stl f, stl x)) (corec_stream (\<lambda>(f, x). shd f (shd x)) (\<lambda>(f, x). False) (\<lambda>(f, x). undefined) (\<lambda>(f, x). (stl f, stl x)) (pure f, x), y)
[PROOF STEP]
by (coinduction arbitrary: x y) auto


[STATEMENT]
lemma list_assn_cong[fundef_cong]:
  "\<lbrakk> xs=xs'; ys=ys'; \<And>x y. \<lbrakk> x\<in>set xs; y\<in>set ys \<rbrakk> \<Longrightarrow> A x y = A' x y \<rbrakk> \<Longrightarrow> list_assn A xs ys = list_assn A' xs' ys'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs = xs'; ys = ys'; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys\<rbrakk> \<Longrightarrow> A x y = A' x y\<rbrakk> \<Longrightarrow> list_assn A xs ys = list_assn A' xs' ys'
[PROOF STEP]
by (induction xs ys arbitrary: xs' ys' rule: list_assn.induct) auto


[STATEMENT]
lemma list_assn_app_one: "list_assn P (l1@[x]) (l1'@[y]) = list_assn P l1 l1' * P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P (l1 @ [x]) (l1' @ [y]) = list_assn P l1 l1' * P x y
[PROOF STEP]
by simp


[STATEMENT]
lemma list_assn_len: "h \<Turnstile> list_assn A xs ys \<Longrightarrow> length xs = length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<Turnstile> list_assn A xs ys \<Longrightarrow> length xs = length ys
[PROOF STEP]
using list_assn_aux_ineq_len
[PROOF STATE]
proof (prove)
using this:
length ?l \<noteq> length ?li \<Longrightarrow> list_assn ?A ?l ?li = false

goal (1 subgoal):
 1. h \<Turnstile> list_assn A xs ys \<Longrightarrow> length xs = length ys
[PROOF STEP]
by fastforce


[STATEMENT]
lemma list_assn_append_Cons_left: "list_assn A (xs@x#ys) zs = (\<exists>\<^sub>A zs1 z zs2. list_assn A xs zs1 * A x z * list_assn A ys zs2 * \<up>(zs1@z#zs2 = zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn A (xs @ x # ys) zs = (\<exists>\<^sub>Azs1 z zs2. list_assn A xs zs1 * A x z * list_assn A ys zs2 * \<up> (zs1 @ z # zs2 = zs))
[PROOF STEP]
by (sep_auto simp add: list_assn_aux_cons_conv list_assn_aux_append_conv1 intro!: ent_iffI)


[STATEMENT]
lemma list_assn_aux_append_Cons:
  shows "length xs = length zsl \<Longrightarrow> list_assn A (xs@x#ys) (zsl@z#zsr) = (list_assn A xs zsl * A x z * list_assn A ys zsr) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length zsl \<Longrightarrow> list_assn A (xs @ x # ys) (zsl @ z # zsr) = list_assn A xs zsl * A x z * list_assn A ys zsr
[PROOF STEP]
by (sep_auto simp add: mult.assoc)


[STATEMENT]
lemma list_assn_prod_split: "list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
[PROOF STEP]
proof(cases "length as = length bs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length as = length bs \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
 2. length as \<noteq> length bs \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length as = length bs

goal (2 subgoals):
 1. length as = length bs \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
 2. length as \<noteq> length bs \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length as = length bs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length as = length bs

goal (1 subgoal):
 1. list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
[PROOF STEP]
proof (induction rule: list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. list_assn (\<lambda>x y. P x y * Q x y) [] [] = list_assn P [] [] * list_assn Q [] []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_assn (\<lambda>x y. P x y * Q x y) xs ys = list_assn P xs ys * list_assn Q xs ys\<rbrakk> \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) = list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. list_assn (\<lambda>x y. P x y * Q x y) [] [] = list_assn P [] [] * list_assn Q [] []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_assn (\<lambda>x y. P x y * Q x y) xs ys = list_assn P xs ys * list_assn Q xs ys\<rbrakk> \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) = list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn (\<lambda>x y. P x y * Q x y) [] [] = list_assn P [] [] * list_assn Q [] []
[PROOF STEP]
by sep_auto
[PROOF STATE]
proof (state)
this:
list_assn (\<lambda>x y. P x y * Q x y) [] [] = list_assn P [] [] * list_assn Q [] []

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_assn (\<lambda>x y. P x y * Q x y) xs ys = list_assn P xs ys * list_assn Q xs ys\<rbrakk> \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) = list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_assn (\<lambda>x y. P x y * Q x y) xs ys = list_assn P xs ys * list_assn Q xs ys\<rbrakk> \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) = list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
[PROOF STEP]
case (Cons x xs y ys)
[PROOF STATE]
proof (state)
this:
length xs = length ys
list_assn (\<lambda>x y. P x y * Q x y) xs ys = list_assn P xs ys * list_assn Q xs ys

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_assn (\<lambda>x y. P x y * Q x y) xs ys = list_assn P xs ys * list_assn Q xs ys\<rbrakk> \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) = list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) = list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
[PROOF STEP]
proof (rule ent_iffI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
 2. list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
 2. list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
list_assn (\<lambda>x y. P x y * Q x y) xs ys = list_assn P xs ys * list_assn Q xs ys

goal (1 subgoal):
 1. list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)
[PROOF STEP]
by sep_auto
[PROOF STATE]
proof (state)
this:
list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)

goal (1 subgoal):
 1. list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
list_assn (\<lambda>x y. P x y * Q x y) xs ys = list_assn P xs ys * list_assn Q xs ys

goal (1 subgoal):
 1. list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys)
[PROOF STEP]
by sep_auto
[PROOF STATE]
proof (state)
this:
list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys) \<Longrightarrow>\<^sub>A list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_assn (\<lambda>x y. P x y * Q x y) (x # xs) (y # ys) = list_assn P (x # xs) (y # ys) * list_assn Q (x # xs) (y # ys)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs

goal (1 subgoal):
 1. length as \<noteq> length bs \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length as \<noteq> length bs \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length as \<noteq> length bs

goal (1 subgoal):
 1. length as \<noteq> length bs \<Longrightarrow> list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length as \<noteq> length bs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length as \<noteq> length bs

goal (1 subgoal):
 1. list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs
[PROOF STEP]
by (simp add: list_assn_aux_ineq_len)
[PROOF STATE]
proof (state)
this:
list_assn (\<lambda>x y. P x y * Q x y) as bs = list_assn P as bs * list_assn Q as bs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_assn_cong[fundef_cong]:
  "\<lbrakk> p=p'; pi=pi'; A (fst p) (fst pi) = A' (fst p) (fst pi); B (snd p) (snd pi) = B' (snd p) (snd pi) \<rbrakk>
    \<Longrightarrow> (A\<times>\<^sub>aB) p pi = (A'\<times>\<^sub>aB') p' pi'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = p'; pi = pi'; A (fst p) (fst pi) = A' (fst p) (fst pi); B (snd p) (snd pi) = B' (snd p) (snd pi)\<rbrakk> \<Longrightarrow> (A \<times>\<^sub>a B) p pi = (A' \<times>\<^sub>a B') p' pi'
[PROOF STEP]
apply (cases p; cases pi)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = p'; pi = pi'; A (fst p) (fst pi) = A' (fst p) (fst pi); B (snd p) (snd pi) = B' (snd p) (snd pi); p = (a, b); pi = (aa, ba)\<rbrakk> \<Longrightarrow> (A \<times>\<^sub>a B) p pi = (A' \<times>\<^sub>a B') p' pi'
[PROOF STEP]
by auto


[STATEMENT]
lemma entails_preI: "(\<And>h. h \<Turnstile> P \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q) \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. h \<Turnstile> P \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q) \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. h \<Turnstile> P \<Longrightarrow> \<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q) \<Longrightarrow> \<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q
[PROOF STEP]
by auto


[STATEMENT]
lemma ent_true_drop_true:
  "P*true\<Longrightarrow>\<^sub>AQ*true \<Longrightarrow> P*R*true\<Longrightarrow>\<^sub>AQ*true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * true \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P * R * true \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
using assn_aci(10) ent_true_drop(1)
[PROOF STATE]
proof (prove)
using this:
?a * ?b * ?c = ?a * ?c * ?b
?P \<Longrightarrow>\<^sub>A ?Q * true \<Longrightarrow> ?P * ?R \<Longrightarrow>\<^sub>A ?Q * true

goal (1 subgoal):
 1. P * true \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P * R * true \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
by presburger


[STATEMENT]
lemma rem_true: "P*true \<Longrightarrow>\<^sub>A Q*true \<Longrightarrow> P \<Longrightarrow>\<^sub>AQ*true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * true \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
using enttD enttI_true
[PROOF STATE]
proof (prove)
using this:
?A \<Longrightarrow>\<^sub>t ?B \<Longrightarrow> ?A \<Longrightarrow>\<^sub>A ?B * true
?P * true \<Longrightarrow>\<^sub>A ?Q * true \<Longrightarrow> ?P \<Longrightarrow>\<^sub>t ?Q

goal (1 subgoal):
 1. P * true \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
by blast


[STATEMENT]
lemma assn_eq_split:
  assumes "B = C"
  shows "B \<Longrightarrow>\<^sub>A C"
  and "C \<Longrightarrow>\<^sub>A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<Longrightarrow>\<^sub>A C &&& C \<Longrightarrow>\<^sub>A B
[PROOF STEP]
by (simp_all add: assms)


[STATEMENT]
lemma ent_ex_inst: "\<exists>\<^sub>Ax. P x \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P y \<Longrightarrow>\<^sub>A Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<^sub>Ax. P x \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P y \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
using ent_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?P \<Longrightarrow>\<^sub>A ?Q; ?Q \<Longrightarrow>\<^sub>A ?R\<rbrakk> \<Longrightarrow> ?P \<Longrightarrow>\<^sub>A ?R

goal (1 subgoal):
 1. \<exists>\<^sub>Ax. P x \<Longrightarrow>\<^sub>A Q \<Longrightarrow> P y \<Longrightarrow>\<^sub>A Q
[PROOF STEP]
by blast


[STATEMENT]
lemma ent_wandI2:
  assumes IMP: "P \<Longrightarrow>\<^sub>A (Q -* R)"
  shows "Q*P \<Longrightarrow>\<^sub>A R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q * P \<Longrightarrow>\<^sub>A R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>A Q -* R

goal (1 subgoal):
 1. Q * P \<Longrightarrow>\<^sub>A R
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q -* R

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> Q * P \<longrightarrow> h \<Turnstile> R
[PROOF STEP]
(*  by (meson assms ent_fwd ent_mp ent_refl fr_rot mod_frame_fwd)*)
[PROOF STATE]
proof (prove)
using this:
\<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q -* R

goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> Q * P \<longrightarrow> h \<Turnstile> R
[PROOF STEP]
proof (clarsimp, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> Q -* R; (a, b) \<Turnstile> Q * P\<rbrakk> \<Longrightarrow> (a, b) \<Turnstile> R
[PROOF STEP]
case (1 h as)
[PROOF STATE]
proof (state)
this:
\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> Q -* R
(h, as) \<Turnstile> Q * P

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> Q -* R; (a, b) \<Turnstile> Q * P\<rbrakk> \<Longrightarrow> (a, b) \<Turnstile> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> Q -* R
(h, as) \<Turnstile> Q * P
[PROOF STEP]
obtain as1 as2 where "as = as1 \<union> as2" "as1 \<inter> as2 = {}" "(h,as1) \<Turnstile> Q" "(h,as2) \<Turnstile> P"
[PROOF STATE]
proof (prove)
using this:
\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> Q -* R
(h, as) \<Turnstile> Q * P

goal (1 subgoal):
 1. (\<And>as1 as2. \<lbrakk>as = as1 \<union> as2; as1 \<inter> as2 = {}; (h, as1) \<Turnstile> Q; (h, as2) \<Turnstile> P\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis mod_star_conv prod.inject)
[PROOF STATE]
proof (state)
this:
as = as1 \<union> as2
as1 \<inter> as2 = {}
(h, as1) \<Turnstile> Q
(h, as2) \<Turnstile> P

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> Q -* R; (a, b) \<Turnstile> Q * P\<rbrakk> \<Longrightarrow> (a, b) \<Turnstile> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as = as1 \<union> as2
as1 \<inter> as2 = {}
(h, as1) \<Turnstile> Q
(h, as2) \<Turnstile> P
[PROOF STEP]
have "(h,as2) \<Turnstile> (Q-*R)"
[PROOF STATE]
proof (prove)
using this:
as = as1 \<union> as2
as1 \<inter> as2 = {}
(h, as1) \<Turnstile> Q
(h, as2) \<Turnstile> P

goal (1 subgoal):
 1. (h, as2) \<Turnstile> Q -* R
[PROOF STEP]
by (simp add: "1"(1))
[PROOF STATE]
proof (state)
this:
(h, as2) \<Turnstile> Q -* R

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> Q -* R; (a, b) \<Turnstile> Q * P\<rbrakk> \<Longrightarrow> (a, b) \<Turnstile> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(h, as2) \<Turnstile> Q -* R
[PROOF STEP]
have "(h,as1\<union>as2) \<Turnstile> Q * (Q-*R)"
[PROOF STATE]
proof (prove)
using this:
(h, as2) \<Turnstile> Q -* R

goal (1 subgoal):
 1. (h, as1 \<union> as2) \<Turnstile> Q * (Q -* R)
[PROOF STEP]
by (simp add: \<open>(h, as1) \<Turnstile> Q\<close> \<open>as1 \<inter> as2 = {}\<close> star_assnI)
[PROOF STATE]
proof (state)
this:
(h, as1 \<union> as2) \<Turnstile> Q * (Q -* R)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (a, b) \<Turnstile> P \<longrightarrow> (a, b) \<Turnstile> Q -* R; (a, b) \<Turnstile> Q * P\<rbrakk> \<Longrightarrow> (a, b) \<Turnstile> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(h, as1 \<union> as2) \<Turnstile> Q * (Q -* R)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(h, as1 \<union> as2) \<Turnstile> Q * (Q -* R)

goal (1 subgoal):
 1. (h, as) \<Turnstile> R
[PROOF STEP]
using \<open>as = as1 \<union> as2\<close> ent_fwd ent_mp
[PROOF STATE]
proof (prove)
using this:
(h, as1 \<union> as2) \<Turnstile> Q * (Q -* R)
as = as1 \<union> as2
\<lbrakk>?h \<Turnstile> ?P; ?P \<Longrightarrow>\<^sub>A ?Q\<rbrakk> \<Longrightarrow> ?h \<Turnstile> ?Q
?P * (?P -* ?Q) \<Longrightarrow>\<^sub>A ?Q

goal (1 subgoal):
 1. (h, as) \<Turnstile> R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(h, as) \<Turnstile> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ent_wand: "(P \<Longrightarrow>\<^sub>A (Q -* R)) = (Q*P \<Longrightarrow>\<^sub>A R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A Q -* R) = (Q * P \<Longrightarrow>\<^sub>A R)
[PROOF STEP]
using ent_wandI2 ent_wandI
[PROOF STATE]
proof (prove)
using this:
?P \<Longrightarrow>\<^sub>A ?Q -* ?R \<Longrightarrow> ?Q * ?P \<Longrightarrow>\<^sub>A ?R
?Q * ?P \<Longrightarrow>\<^sub>A ?R \<Longrightarrow> ?P \<Longrightarrow>\<^sub>A ?Q -* ?R

goal (1 subgoal):
 1. (P \<Longrightarrow>\<^sub>A Q -* R) = (Q * P \<Longrightarrow>\<^sub>A R)
[PROOF STEP]
by blast


[STATEMENT]
lemma wand_ent_trans:
  assumes "P' \<Longrightarrow>\<^sub>A P"
      and "Q \<Longrightarrow>\<^sub>A Q'"
    shows "P -* Q \<Longrightarrow>\<^sub>A P' -* Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P -* Q \<Longrightarrow>\<^sub>A P' -* Q'
[PROOF STEP]
by (meson assms(1) assms(2) ent_wand ent_frame_fwd ent_refl ent_trans)


[STATEMENT]
lemma wand_elim: "(P -* Q) * (Q -* R) \<Longrightarrow>\<^sub>A (P -* R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P -* Q) * (Q -* R) \<Longrightarrow>\<^sub>A P -* R
[PROOF STEP]
by (metis ent_wand ent_frame_fwd ent_mp ent_refl star_assoc)


[STATEMENT]
lemma emp_wand_same: "emp \<Longrightarrow>\<^sub>A (H -* H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emp \<Longrightarrow>\<^sub>A H -* H
[PROOF STEP]
by (simp add: ent_wandI)


[STATEMENT]
lemma emp_wand_equal: "(emp -* H) = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emp -* H = H
[PROOF STEP]
apply(intro ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. emp -* H \<Longrightarrow>\<^sub>A H
 2. H \<Longrightarrow>\<^sub>A emp -* H
[PROOF STEP]
apply (metis ent_mp norm_assertion_simps(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<Longrightarrow>\<^sub>A emp -* H
[PROOF STEP]
by (simp add: ent_wandI)


[STATEMENT]
lemma pure_wand_equal: "P \<Longrightarrow> (\<up>(P) -* H) = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> \<up> P -* H = H
[PROOF STEP]
by (simp add: emp_wand_equal)


[STATEMENT]
lemma pure_wand_ent: "(P \<Longrightarrow> (H1 \<Longrightarrow>\<^sub>A H2)) \<Longrightarrow> H1 \<Longrightarrow>\<^sub>A \<up>(P) -* H2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> H1 \<Longrightarrow>\<^sub>A H2) \<Longrightarrow> H1 \<Longrightarrow>\<^sub>A \<up> P -* H2
[PROOF STEP]
by (simp add: ent_wand)


[STATEMENT]
lemma "\<up>(P \<longrightarrow> Q) \<Longrightarrow>\<^sub>A (\<up>(P) -* \<up>(Q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up> (P \<longrightarrow> Q) \<Longrightarrow>\<^sub>A \<up> P -* \<up> Q
[PROOF STEP]
by (simp add: pure_wand_ent)


[STATEMENT]
lemma wand_uncurry: "(P*Q) -* R \<Longrightarrow>\<^sub>A P -* (Q -* R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * Q -* R \<Longrightarrow>\<^sub>A P -* (Q -* R)
[PROOF STEP]
by (simp add: assn_aci ent_mp ent_wandI fr_rot)


[STATEMENT]
lemma wand_absorb: "(P -* Q) * R \<Longrightarrow>\<^sub>A (P -* (Q * R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P -* Q) * R \<Longrightarrow>\<^sub>A P -* Q * R
[PROOF STEP]
by (smt (z3) ent_mp ent_refl ent_star_mono ent_wandI star_aci(2) star_aci(3))


[STATEMENT]
lemma wand_ent_self: "P \<Longrightarrow>\<^sub>A Q -* (Q * P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q -* Q * P
[PROOF STEP]
by (simp add: ent_wandI)


[STATEMENT]
lemma wand_ent_cancel: "P * ((P * Q) -* R) \<Longrightarrow>\<^sub>A Q -* R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P * (P * Q -* R) \<Longrightarrow>\<^sub>A Q -* R
[PROOF STEP]
by (simp add: ent_wandI2 wand_uncurry)


[STATEMENT]
lemma "\<exists>R. Q * R \<Longrightarrow>\<^sub>A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>R. Q * R \<Longrightarrow>\<^sub>A P
[PROOF STEP]
using ent_mp
[PROOF STATE]
proof (prove)
using this:
?P * (?P -* ?Q) \<Longrightarrow>\<^sub>A ?Q

goal (1 subgoal):
 1. \<exists>R. Q * R \<Longrightarrow>\<^sub>A P
[PROOF STEP]
by auto


[STATEMENT]
lemma "P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P = Q * (Q -* P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P = Q * (Q -* P)
[PROOF STEP]
apply(intro ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * (Q -* P)
 2. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> Q * (Q -* P) \<Longrightarrow>\<^sub>A P
[PROOF STEP]
proof(goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * (Q -* P)
 2. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> Q * (Q -* P) \<Longrightarrow>\<^sub>A P
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>A Q * true

goal (2 subgoals):
 1. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * (Q -* P)
 2. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> Q * (Q -* P) \<Longrightarrow>\<^sub>A P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<Longrightarrow>\<^sub>A Q * true
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<Longrightarrow>\<^sub>A Q * true

goal (1 subgoal):
 1. Q * (Q -* P) \<Longrightarrow>\<^sub>A P
[PROOF STEP]
by (simp add: ent_mp)
[PROOF STATE]
proof (state)
this:
Q * (Q -* P) \<Longrightarrow>\<^sub>A P

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * (Q -* P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * (Q -* P)
[PROOF STEP]
case test: 1
[PROOF STATE]
proof (state)
this:
P \<Longrightarrow>\<^sub>A Q * true

goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q * true \<Longrightarrow> P \<Longrightarrow>\<^sub>A Q * (Q -* P)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow>\<^sub>A Q * (Q -* P)
[PROOF STEP]
unfolding entails_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h. h \<Turnstile> P \<longrightarrow> h \<Turnstile> Q * (Q -* P)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> P \<Longrightarrow> (a, b) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> P \<Longrightarrow> (a, b) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
case (1 a b)
[PROOF STATE]
proof (state)
this:
(a, b) \<Turnstile> P

goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> P \<Longrightarrow> (a, b) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<Turnstile> P
[PROOF STEP]
have "(a,b) \<Turnstile> Q * true"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<Turnstile> P

goal (1 subgoal):
 1. (a, b) \<Turnstile> Q * true
[PROOF STEP]
using test entails_def
[PROOF STATE]
proof (prove)
using this:
(a, b) \<Turnstile> P
P \<Longrightarrow>\<^sub>A Q * true
?P \<Longrightarrow>\<^sub>A ?Q \<equiv> \<forall>h. h \<Turnstile> ?P \<longrightarrow> h \<Turnstile> ?Q

goal (1 subgoal):
 1. (a, b) \<Turnstile> Q * true
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(a, b) \<Turnstile> Q * true

goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> P \<Longrightarrow> (a, b) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<Turnstile> Q * true
[PROOF STEP]
obtain h as1 as2 where *:
        "(a,b) = (h, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (h, as1) \<Turnstile> Q \<and> (h, as2) \<Turnstile> true"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<Turnstile> Q * true

goal (1 subgoal):
 1. (\<And>h as1 as2. (a, b) = (h, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (h, as1) \<Turnstile> Q \<and> (h, as2) \<Turnstile> true \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mod_star_conv
[PROOF STATE]
proof (prove)
using this:
(a, b) \<Turnstile> Q * true
(?h \<Turnstile> ?A * ?B) = (\<exists>hr as1 as2. ?h = (hr, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (hr, as1) \<Turnstile> ?A \<and> (hr, as2) \<Turnstile> ?B)

goal (1 subgoal):
 1. (\<And>h as1 as2. (a, b) = (h, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (h, as1) \<Turnstile> Q \<and> (h, as2) \<Turnstile> true \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a, b) = (h, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (h, as1) \<Turnstile> Q \<and> (h, as2) \<Turnstile> true

goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> P \<Longrightarrow> (a, b) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a, b) = (h, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (h, as1) \<Turnstile> Q \<and> (h, as2) \<Turnstile> true
[PROOF STEP]
have "(h, as1 \<union> as2) \<Turnstile> P" "(a,b) = (h, as1 \<union> as2)"
[PROOF STATE]
proof (prove)
using this:
(a, b) = (h, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (h, as1) \<Turnstile> Q \<and> (h, as2) \<Turnstile> true

goal (1 subgoal):
 1. (h, as1 \<union> as2) \<Turnstile> P &&& (a, b) = (h, as1 \<union> as2)
[PROOF STEP]
using "1"
[PROOF STATE]
proof (prove)
using this:
(a, b) = (h, as1 \<union> as2) \<and> as1 \<inter> as2 = {} \<and> (h, as1) \<Turnstile> Q \<and> (h, as2) \<Turnstile> true
(a, b) \<Turnstile> P

goal (1 subgoal):
 1. (h, as1 \<union> as2) \<Turnstile> P &&& (a, b) = (h, as1 \<union> as2)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
(h, as1 \<union> as2) \<Turnstile> P
(a, b) = (h, as1 \<union> as2)

goal (1 subgoal):
 1. \<And>a b. (a, b) \<Turnstile> P \<Longrightarrow> (a, b) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(h, as1 \<union> as2) \<Turnstile> P
(a, b) = (h, as1 \<union> as2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(h, as1 \<union> as2) \<Turnstile> P
(a, b) = (h, as1 \<union> as2)

goal (1 subgoal):
 1. (a, b) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2\<rbrakk> \<Longrightarrow> (h, as1 \<union> as2) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
thm star_assnI
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2\<rbrakk> \<Longrightarrow> (h, as1 \<union> as2) \<Turnstile> Q * (Q -* P)
[PROOF STEP]
apply(intro star_assnI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2\<rbrakk> \<Longrightarrow> (h, as1) \<Turnstile> Q
 2. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2\<rbrakk> \<Longrightarrow> (h, as2) \<Turnstile> Q -* P
 3. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2\<rbrakk> \<Longrightarrow> as1 \<inter> as2 = {}
[PROOF STEP]
apply (simp_all add: *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2\<rbrakk> \<Longrightarrow> (h, as2) \<Turnstile> Q -* P
[PROOF STEP]
apply(intro wand_assnI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2\<rbrakk> \<Longrightarrow> in_range (h, as2)
 2. \<And>h' as'. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2; as2 \<inter> as' = {}; relH as2 h h'; in_range (h', as2); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', as2 \<union> as') \<Turnstile> P
[PROOF STEP]
apply (meson "*" models_in_range)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h' as'. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; a = h \<and> b = as1 \<union> as2; as2 \<inter> as' = {}; relH as2 h h'; in_range (h', as2); (h', as') \<Turnstile> Q\<rbrakk> \<Longrightarrow> (h', as2 \<union> as') \<Turnstile> P
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h' as'. \<lbrakk>(h, as1 \<union> as2) \<Turnstile> P; as2 \<inter> as' = {}; relH as2 h h'; in_range (h', as2); (h', as') \<Turnstile> Q; a = h; b = as1 \<union> as2\<rbrakk> \<Longrightarrow> (h', as2 \<union> as') \<Turnstile> P
[PROOF STEP]
oops


[STATEMENT]
lemma diamond_x_1:
  "|x>1 = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (1::'a) = d x
[PROOF STEP]
by (simp add: diamond_def)


[STATEMENT]
lemma diamond_x_d:
  "|x>d(y) = d(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > d y = d (x * y)
[PROOF STEP]
using d_mult_d diamond_def
[PROOF STATE]
proof (prove)
using this:
d (?x * ?y) = d (?x * d ?y)
| ?x > ?y = d (?x * ?y)

goal (1 subgoal):
 1. | x > d y = d (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_x_und:
  "|x>d(y) = |x>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > d y = | x > y
[PROOF STEP]
using diamond_x_d diamond_def
[PROOF STATE]
proof (prove)
using this:
| ?x > d ?y = d (?x * ?y)
| ?x > ?y = d (?x * ?y)

goal (1 subgoal):
 1. | x > d y = | x > y
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_d_closed:
  "|x>y = d( |x>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y = d (| x > y)
[PROOF STEP]
by (simp add: d_involutive diamond_def)


[STATEMENT]
lemma diamond_bot_y:
  "|bot>y = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | bot > y = bot
[PROOF STEP]
by (simp add: d_zero diamond_def)


[STATEMENT]
lemma diamond_1_y:
  "|1>y = d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) > y = d y
[PROOF STEP]
by (simp add: diamond_def)


[STATEMENT]
lemma diamond_1_d:
  "|1>d(y) = d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) > d y = d y
[PROOF STEP]
by (simp add: diamond_1_y diamond_x_und)


[STATEMENT]
lemma diamond_d_y:
  "|d(x)>y = d(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x > y = d x * d y
[PROOF STEP]
by (simp add: d_export diamond_def)


[STATEMENT]
lemma diamond_d_bot:
  "|d(x)>bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x > bot = bot
[PROOF STEP]
by (metis diamond_bot_y diamond_d_y d_commutative d_zero)


[STATEMENT]
lemma diamond_d_1:
  "|d(x)>1 = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x > (1::'a) = d x
[PROOF STEP]
by (simp add: diamond_x_1 d_involutive)


[STATEMENT]
lemma diamond_d_d:
  "|d(x)>d(y) = d(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x > d y = d x * d y
[PROOF STEP]
by (simp add: diamond_d_y diamond_x_und)


[STATEMENT]
lemma diamond_d_d_same:
  "|d(x)>d(x) = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x > d x = d x
[PROOF STEP]
by (simp add: diamond_d_d d_idempotent)


[STATEMENT]
lemma diamond_left_dist_sup:
  "|x \<squnion> y>z = |x>z \<squnion> |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x \<squnion> y > z = | x > z \<squnion> | y > z
[PROOF STEP]
by (simp add: d_dist_sup diamond_def mult_right_dist_sup)


[STATEMENT]
lemma diamond_right_sub_dist_sup:
  "|x>y \<squnion> |x>z \<le> |x>(y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y \<squnion> | x > z \<le> | x > (y \<squnion> z)
[PROOF STEP]
by (metis d_dist_sup diamond_def le_iff_sup mult_left_sub_dist_sup)


[STATEMENT]
lemma diamond_left_mult:
  "|x * y>z = |x>|y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * y > z = | x > | y > z
[PROOF STEP]
using diamond_x_und diamond_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
| ?x > d ?y = | ?x > ?y
| ?x > ?y = d (?x * ?y)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | x * y > z = | x > | y > z
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_right_mult:
  "|x>(y * z) = |x>|y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (y * z) = | x > | y > z
[PROOF STEP]
using diamond_associative diamond_left_mult
[PROOF STATE]
proof (prove)
using this:
| ?x * ?y > ?z = | ?x > (?y * ?z)
| ?x * ?y > ?z = | ?x > | ?y > ?z

goal (1 subgoal):
 1. | x > (y * z) = | x > | y > z
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_d_export:
  "|d(x) * y>z = d(x) * |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x * y > z = d x * | y > z
[PROOF STEP]
using diamond_d_y diamond_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
| d ?x > ?y = d ?x * d ?y
| ?x > ?y = d (?x * ?y)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | d x * y > z = d x * | y > z
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_diamond_export:
  "||x>y>z = |x>y * |z>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | | x > y > z = | x > y * | z > (1::'a)
[PROOF STEP]
using diamond_d_y diamond_def
[PROOF STATE]
proof (prove)
using this:
| d ?x > ?y = d ?x * d ?y
| ?x > ?y = d (?x * ?y)

goal (1 subgoal):
 1. | | x > y > z = | x > y * | z > (1::'a)
[PROOF STEP]
by force


[STATEMENT]
lemma diamond_left_isotone:
  "x \<le> y \<Longrightarrow> |x>z \<le> |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> | x > z \<le> | y > z
[PROOF STEP]
by (metis diamond_left_dist_sup le_iff_sup)


[STATEMENT]
lemma diamond_right_isotone:
  "y \<le> z \<Longrightarrow> |x>y \<le> |x>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> z \<Longrightarrow> | x > y \<le> | x > z
[PROOF STEP]
by (metis diamond_right_sub_dist_sup le_iff_sup le_sup_iff)


[STATEMENT]
lemma diamond_isotone:
  "w \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> |w>x \<le> |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> | w > x \<le> | y > z
[PROOF STEP]
by (meson diamond_left_isotone diamond_right_isotone order_trans)


[STATEMENT]
lemma diamond_left_upper_bound:
  "|x>y \<le> |x \<squnion> z>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y \<le> | x \<squnion> z > y
[PROOF STEP]
by (simp add: diamond_left_isotone)


[STATEMENT]
lemma diamond_right_upper_bound:
  "|x>y \<le> |x>(y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y \<le> | x > (y \<squnion> z)
[PROOF STEP]
by (simp add: diamond_right_isotone)


[STATEMENT]
lemma diamond_lower_bound_right:
  "|x>(d(y) * d(z)) \<le> |x>d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (d y * d z) \<le> | x > d y
[PROOF STEP]
by (simp add: diamond_right_isotone d_mult_left_lower_bound)


[STATEMENT]
lemma diamond_lower_bound_left:
  "|x>(d(y) * d(z)) \<le> |x>d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (d y * d z) \<le> | x > d z
[PROOF STEP]
using diamond_lower_bound_right d_commutative
[PROOF STATE]
proof (prove)
using this:
| ?x > (d ?y * d ?z) \<le> | ?x > d ?y
d ?x * d ?y = d ?y * d ?x

goal (1 subgoal):
 1. | x > (d y * d z) \<le> | x > d z
[PROOF STEP]
by force


[STATEMENT]
lemma diamond_right_sub_dist_mult:
  "|x>(d(y) * d(z)) \<le> |x>d(y) * |x>d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (d y * d z) \<le> | x > d y * | x > d z
[PROOF STEP]
using diamond_lower_bound_left diamond_lower_bound_right d_mult_greatest_lower_bound diamond_def
[PROOF STATE]
proof (prove)
using this:
| ?x > (d ?y * d ?z) \<le> | ?x > d ?z
| ?x > (d ?y * d ?z) \<le> | ?x > d ?y
(d ?x \<le> d ?y * d ?z) = (d ?x \<le> d ?y \<and> d ?x \<le> d ?z)
| ?x > ?y = d (?x * ?y)

goal (1 subgoal):
 1. | x > (d y * d z) \<le> | x > d y * | x > d z
[PROOF STEP]
by force


[STATEMENT]
lemma diamond_demodalisation_1:
  "d(x) * |y>z \<le> Z \<longleftrightarrow> d(x) * y * d(z) \<le> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * | y > z \<le> Z) = (d x * y * d z \<le> Z)
[PROOF STEP]
by (metis d_weak_locality diamond_def mult_assoc)


[STATEMENT]
lemma diamond_demodalisation_3:
  "|x>y \<le> d(z) \<longleftrightarrow> x * d(y) \<le> d(z) * x \<squnion> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (| x > y \<le> d z) = (x * d y \<le> d z * x \<squnion> Z)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. | x > y \<le> d z \<Longrightarrow> x * d y \<le> d z * x \<squnion> Z
 2. x * d y \<le> d z * x \<squnion> Z \<Longrightarrow> | x > y \<le> d z
[PROOF STEP]
apply (smt (verit) sup_commute sup_right_isotone d_below_one d_restrict diamond_def diamond_x_und mult_left_isotone mult_right_isotone mult_1_right order_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * d y \<le> d z * x \<squnion> Z \<Longrightarrow> | x > y \<le> d z
[PROOF STEP]
by (smt sup_commute sup_bot_left d_Z d_commutative d_dist_sup d_involutive d_mult_sub d_plus_left_upper_bound diamond_d_y diamond_def diamond_x_und le_iff_sup order_trans)


[STATEMENT]
lemma diamond_d_export_2:
  "|d(x) * y>z = d(x) * |d(x) * y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x * y > z = d x * | d x * y > z
[PROOF STEP]
by (metis diamond_d_export diamond_left_mult d_idempotent)


[STATEMENT]
lemma diamond_d_promote:
  "|x * d(y)>z = |x * d(y)>(d(y) * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * d y > z = | x * d y > (d y * z)
[PROOF STEP]
by (metis d_idempotent diamond_def mult_assoc)


[STATEMENT]
lemma diamond_d_import_iff:
  "d(x) \<le> |y>z \<longleftrightarrow> d(x) \<le> |d(x) * y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<le> | y > z) = (d x \<le> | d x * y > z)
[PROOF STEP]
by (metis diamond_d_export diamond_d_y d_order diamond_def order.eq_iff)


[STATEMENT]
lemma diamond_d_import_iff_2:
  "d(x) * d(y) \<le> |z>w \<longleftrightarrow> d(x) * d(y) \<le> |d(y) * z>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * d y \<le> | z > w) = (d x * d y \<le> | d y * z > w)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d x * d y \<le> | z > w \<Longrightarrow> d x * d y \<le> | d y * z > w
 2. d x * d y \<le> | d y * z > w \<Longrightarrow> d x * d y \<le> | z > w
[PROOF STEP]
apply (metis diamond_associative d_export d_mult_greatest_lower_bound diamond_def order.refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * d y \<le> | d y * z > w \<Longrightarrow> d x * d y \<le> | z > w
[PROOF STEP]
by (metis diamond_d_y d_mult_greatest_lower_bound diamond_def mult_assoc)


[STATEMENT]
lemma box_diamond:
  "|x]y = a( |x>a(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] y = a (| x > a y)
[PROOF STEP]
by (simp add: box_def d_a_closed diamond_def)


[STATEMENT]
lemma diamond_box:
  "|x>y = a( |x]a(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y = a (| x ] a y)
[PROOF STEP]
using box_def d_def d_mult_d diamond_def
[PROOF STATE]
proof (prove)
using this:
| ?x ] ?y = a (?x * a ?y)
d ?x = a (a ?x)
d (?x * ?y) = d (?x * d ?y)
| ?x > ?y = d (?x * ?y)

goal (1 subgoal):
 1. | x > y = a (| x ] a y)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_x_bot:
  "|x]bot = a(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] bot = a x
[PROOF STEP]
by (metis box_def mult_1_right one_def)


[STATEMENT]
lemma box_x_1:
  "|x]1 = a(x * bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (1::'a) = a (x * bot)
[PROOF STEP]
by (simp add: box_def)


[STATEMENT]
lemma box_x_d:
  "|x]d(y) = a(x * a(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] d y = a (x * a y)
[PROOF STEP]
by (simp add: box_def d_a_closed)


[STATEMENT]
lemma box_x_und:
  "|x]d(y) = |x]y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] d y = | x ] y
[PROOF STEP]
by (simp add: box_diamond d_a_closed)


[STATEMENT]
lemma box_x_a:
  "|x]a(y) = a(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] a y = a (x * y)
[PROOF STEP]
using a_mult_d box_def
[PROOF STATE]
proof (prove)
using this:
a (?x * ?y) = a (?x * a (a ?y))
| ?x ] ?y = a (?x * a ?y)

goal (1 subgoal):
 1. | x ] a y = a (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_bot_y:
  "|bot]y = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | bot ] y = (1::'a)
[PROOF STEP]
using box_def
[PROOF STATE]
proof (prove)
using this:
| ?x ] ?y = a (?x * a ?y)

goal (1 subgoal):
 1. | bot ] y = (1::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_1_y:
  "|1]y = d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) ] y = d y
[PROOF STEP]
by (simp add: box_def d_def)


[STATEMENT]
lemma box_1_d:
  "|1]d(y) = d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) ] d y = d y
[PROOF STEP]
by (simp add: box_1_y box_x_und)


[STATEMENT]
lemma box_1_a:
  "|1]a(y) = a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) ] a y = a y
[PROOF STEP]
by (simp add: box_x_a)


[STATEMENT]
lemma box_d_y:
  "|d(x)]y = a(x) \<squnion> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x ] y = a x \<squnion> d y
[PROOF STEP]
using a_export_a box_def d_def
[PROOF STATE]
proof (prove)
using this:
a (a ?x * ?y) = d ?x \<squnion> a ?y
| ?x ] ?y = a (?x * a ?y)
d ?x = a (a ?x)

goal (1 subgoal):
 1. | d x ] y = a x \<squnion> d y
[PROOF STEP]
by auto


[STATEMENT]
lemma box_a_y:
  "|a(x)]y = d(x) \<squnion> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x ] y = d x \<squnion> d y
[PROOF STEP]
by (simp add: a_mult_deMorgan_1 box_def)


[STATEMENT]
lemma box_d_bot:
  "|d(x)]bot = a(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x ] bot = a x
[PROOF STEP]
by (simp add: box_x_bot d_a_closed)


[STATEMENT]
lemma box_a_bot:
  "|a(x)]bot = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x ] bot = d x
[PROOF STEP]
by (simp add: box_x_bot d_def)


[STATEMENT]
lemma box_d_1:
  "|d(x)]1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x ] (1::'a) = (1::'a)
[PROOF STEP]
by (simp add: box_d_y d_one_one)


[STATEMENT]
lemma box_a_1:
  "|a(x)]1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x ] (1::'a) = (1::'a)
[PROOF STEP]
by (simp add: box_x_1)


[STATEMENT]
lemma box_d_d:
  "|d(x)]d(y) = a(x) \<squnion> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x ] d y = a x \<squnion> d y
[PROOF STEP]
by (simp add: box_d_y box_x_und)


[STATEMENT]
lemma box_a_d:
  "|a(x)]d(y) = d(x) \<squnion> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x ] d y = d x \<squnion> d y
[PROOF STEP]
by (simp add: box_a_y box_x_und)


[STATEMENT]
lemma box_d_a:
  "|d(x)]a(y) = a(x) \<squnion> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x ] a y = a x \<squnion> a y
[PROOF STEP]
by (simp add: box_x_a a_export_d)


[STATEMENT]
lemma box_a_a:
  "|a(x)]a(y) = d(x) \<squnion> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x ] a y = d x \<squnion> a y
[PROOF STEP]
by (simp add: box_a_y a_d_closed)


[STATEMENT]
lemma box_d_d_same:
  "|d(x)]d(x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x ] d x = (1::'a)
[PROOF STEP]
using box_x_d d_complement_zero
[PROOF STATE]
proof (prove)
using this:
| ?x ] d ?y = a (?x * a ?y)
d ?x * a ?x = bot

goal (1 subgoal):
 1. | d x ] d x = (1::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_a_a_same:
  "|a(x)]a(x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x ] a x = (1::'a)
[PROOF STEP]
by (simp add: box_def)


[STATEMENT]
lemma box_d_below_box:
  "d(x) \<le> |d(y)]d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<le> | d y ] d x
[PROOF STEP]
by (simp add: box_d_d)


[STATEMENT]
lemma box_d_closed:
  "|x]y = d( |x]y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] y = d (| x ] y)
[PROOF STEP]
by (simp add: a_d_closed box_def)


[STATEMENT]
lemma box_deMorgan_1:
  "a( |x]y) = |x>a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (| x ] y) = | x > a y
[PROOF STEP]
by (simp add: diamond_box box_def)


[STATEMENT]
lemma box_deMorgan_2:
  "a( |x>y) = |x]a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (| x > y) = | x ] a y
[PROOF STEP]
using box_x_a d_a_closed diamond_def
[PROOF STATE]
proof (prove)
using this:
| ?x ] a ?y = a (?x * ?y)
a (d ?x) = a ?x
| ?x > ?y = d (?x * ?y)

goal (1 subgoal):
 1. a (| x > y) = | x ] a y
[PROOF STEP]
by auto


[STATEMENT]
lemma box_left_dist_sup:
  "|x \<squnion> y]z = |x]z * |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x \<squnion> y ] z = | x ] z * | y ] z
[PROOF STEP]
by (simp add: a_dist_sup box_def mult_right_dist_sup)


[STATEMENT]
lemma box_right_dist_sup:
  "|x](y \<squnion> z) = a(x * a(y) * a(z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (y \<squnion> z) = a (x * a y * a z)
[PROOF STEP]
by (simp add: a_dist_sup box_def mult_assoc)


[STATEMENT]
lemma box_associative:
  "|x * y]z = a(x * y * a(z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * y ] z = a (x * y * a z)
[PROOF STEP]
by (simp add: box_def)


[STATEMENT]
lemma box_left_mult:
  "|x * y]z = |x]|y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * y ] z = | x ] | y ] z
[PROOF STEP]
using box_x_a box_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
| ?x ] a ?y = a (?x * ?y)
| ?x ] ?y = a (?x * a ?y)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | x * y ] z = | x ] | y ] z
[PROOF STEP]
by force


[STATEMENT]
lemma box_right_mult:
  "|x](y * z) = a(x * a(y * z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (y * z) = a (x * a (y * z))
[PROOF STEP]
by (simp add: box_def)


[STATEMENT]
lemma box_right_submult_d_d:
  "|x](d(y) * d(z)) \<le> |x]d(y) * |x]d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (d y * d z) \<le> | x ] d y * | x ] d z
[PROOF STEP]
by (smt a_antitone a_dist_sup a_export_d box_diamond d_a_closed diamond_def mult_left_sub_dist_sup)


[STATEMENT]
lemma box_right_submult_a_d:
  "|x](a(y) * d(z)) \<le> |x]a(y) * |x]d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (a y * d z) \<le> | x ] a y * | x ] d z
[PROOF STEP]
by (metis box_right_submult_d_d a_d_closed)


[STATEMENT]
lemma box_right_submult_d_a:
  "|x](d(y) * a(z)) \<le> |x]d(y) * |x]a(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (d y * a z) \<le> | x ] d y * | x ] a z
[PROOF STEP]
using box_right_submult_a_d box_x_a d_def tests_dual.sub_commutative
[PROOF STATE]
proof (prove)
using this:
| ?x ] (a ?y * d ?z) \<le> | ?x ] a ?y * | ?x ] d ?z
| ?x ] a ?y = a (?x * ?y)
d ?x = a (a ?x)
a ?x * a ?y = a ?y * a ?x

goal (1 subgoal):
 1. | x ] (d y * a z) \<le> | x ] d y * | x ] a z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_right_submult_a_a:
  "|x](a(y) * a(z)) \<le> |x]a(y) * |x]a(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (a y * a z) \<le> | x ] a y * | x ] a z
[PROOF STEP]
by (metis box_right_submult_d_d a_d_closed)


[STATEMENT]
lemma box_d_export:
  "|d(x) * y]z = a(x) \<squnion> |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x * y ] z = a x \<squnion> | y ] z
[PROOF STEP]
by (simp add: a_export_d box_def mult_assoc)


[STATEMENT]
lemma box_a_export:
  "|a(x) * y]z = d(x) \<squnion> |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x * y ] z = d x \<squnion> | y ] z
[PROOF STEP]
using box_a_y box_d_closed box_left_mult
[PROOF STATE]
proof (prove)
using this:
| a ?x ] ?y = d ?x \<squnion> d ?y
| ?x ] ?y = d (| ?x ] ?y)
| ?x * ?y ] ?z = | ?x ] | ?y ] ?z

goal (1 subgoal):
 1. | a x * y ] z = d x \<squnion> | y ] z
[PROOF STEP]
by auto


[STATEMENT]
lemma box_left_antitone:
  "y \<le> x \<Longrightarrow> |x]z \<le> |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> x \<Longrightarrow> | x ] z \<le> | y ] z
[PROOF STEP]
by (metis a_antitone box_def mult_left_isotone)


[STATEMENT]
lemma box_right_isotone:
  "y \<le> z \<Longrightarrow> |x]y \<le> |x]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> z \<Longrightarrow> | x ] y \<le> | x ] z
[PROOF STEP]
by (metis a_antitone box_def mult_right_isotone)


[STATEMENT]
lemma box_antitone_isotone:
  "y \<le> w \<Longrightarrow> x \<le> z \<Longrightarrow> |w]x \<le> |y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<le> w; x \<le> z\<rbrakk> \<Longrightarrow> | w ] x \<le> | y ] z
[PROOF STEP]
by (meson box_left_antitone box_right_isotone order_trans)


[STATEMENT]
lemma diamond_1_a:
  "|1>a(y) = a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) > a y = a y
[PROOF STEP]
by (simp add: d_def diamond_1_y)


[STATEMENT]
lemma diamond_a_y:
  "|a(x)>y = a(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x > y = a x * d y
[PROOF STEP]
by (metis a_d_closed diamond_d_y)


[STATEMENT]
lemma diamond_a_bot:
  "|a(x)>bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x > bot = bot
[PROOF STEP]
by (simp add: diamond_a_y d_zero)


[STATEMENT]
lemma diamond_a_1:
  "|a(x)>1 = a(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x > (1::'a) = a x
[PROOF STEP]
by (simp add: d_def diamond_x_1)


[STATEMENT]
lemma diamond_a_d:
  "|a(x)>d(y) = a(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x > d y = a x * d y
[PROOF STEP]
by (simp add: diamond_a_y diamond_x_und)


[STATEMENT]
lemma diamond_d_a:
  "|d(x)>a(y) = d(x) * a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | d x > a y = d x * a y
[PROOF STEP]
by (simp add: a_d_closed diamond_d_y)


[STATEMENT]
lemma diamond_a_a:
  "|a(x)>a(y) = a(x) * a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x > a y = a x * a y
[PROOF STEP]
by (simp add: a_mult_closed diamond_def)


[STATEMENT]
lemma diamond_a_a_same:
  "|a(x)>a(x) = a(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x > a x = a x
[PROOF STEP]
by (simp add: diamond_a_a)


[STATEMENT]
lemma diamond_a_export:
  "|a(x) * y>z = a(x) * |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | a x * y > z = a x * | y > z
[PROOF STEP]
using diamond_a_y diamond_associative diamond_def
[PROOF STATE]
proof (prove)
using this:
| a ?x > ?y = a ?x * d ?y
| ?x * ?y > ?z = | ?x > (?y * ?z)
| ?x > ?y = d (?x * ?y)

goal (1 subgoal):
 1. | a x * y > z = a x * | y > z
[PROOF STEP]
by auto


[STATEMENT]
lemma a_box_a_a:
  "a(p) * |a(p)]a(q) = a(p) * a(q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a p * | a p ] a q = a p * a q
[PROOF STEP]
using box_a_a box_a_bot box_x_bot tests_dual.sup_complement_intro
[PROOF STATE]
proof (prove)
using this:
| a ?x ] a ?y = d ?x \<squnion> a ?y
| a ?x ] bot = d ?x
| ?x ] bot = a ?x
a ?x * a ?y = a ?x * (a (a ?x) \<squnion> a ?y)

goal (1 subgoal):
 1. a p * | a p ] a q = a p * a q
[PROOF STEP]
by auto


[STATEMENT]
lemma box_left_lower_bound:
  "|x \<squnion> y]z \<le> |x]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x \<squnion> y ] z \<le> | x ] z
[PROOF STEP]
by (simp add: box_left_antitone)


[STATEMENT]
lemma box_right_upper_bound:
  "|x]y \<le> |x](y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] y \<le> | x ] (y \<squnion> z)
[PROOF STEP]
by (simp add: box_right_isotone)


[STATEMENT]
lemma box_lower_bound_right:
  "|x](d(y) * d(z)) \<le> |x]d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (d y * d z) \<le> | x ] d y
[PROOF STEP]
by (simp add: box_right_isotone d_mult_left_lower_bound)


[STATEMENT]
lemma box_lower_bound_left:
  "|x](d(y) * d(z)) \<le> |x]d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (d y * d z) \<le> | x ] d z
[PROOF STEP]
by (simp add: box_right_isotone d_restrict_iff_1)


[STATEMENT]
lemma box_d_import:
  "d(x) * |y]z = d(x) * |d(x) * y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * | y ] z = d x * | d x * y ] z
[PROOF STEP]
using a_box_a_a box_left_mult box_def d_def
[PROOF STATE]
proof (prove)
using this:
a ?p * | a ?p ] a ?q = a ?p * a ?q
| ?x * ?y ] ?z = | ?x ] | ?y ] ?z
| ?x ] ?y = a (?x * a ?y)
d ?x = a (a ?x)

goal (1 subgoal):
 1. d x * | y ] z = d x * | d x * y ] z
[PROOF STEP]
by force


[STATEMENT]
lemma box_d_promote:
  "|x * d(y)]z = |x * d(y)](d(y) * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * d y ] z = | x * d y ] (d y * z)
[PROOF STEP]
using a_box_a_a box_x_a box_def d_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
a ?p * | a ?p ] a ?q = a ?p * a ?q
| ?x ] a ?y = a (?x * ?y)
| ?x ] ?y = a (?x * a ?y)
d ?x = a (a ?x)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | x * d y ] z = | x * d y ] (d y * z)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_d_import_iff:
  "d(x) \<le> |y]z \<longleftrightarrow> d(x) \<le> |d(x) * y]z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<le> | y ] z) = (d x \<le> | d x * y ] z)
[PROOF STEP]
using box_d_export box_def d_def tests_dual.shunting
[PROOF STATE]
proof (prove)
using this:
| d ?x * ?y ] ?z = a ?x \<squnion> | ?y ] ?z
| ?x ] ?y = a (?x * a ?y)
d ?x = a (a ?x)
(a ?z \<le> a ?x \<squnion> a ?y) = (a (a ?x) * a ?z \<le> a ?y)

goal (1 subgoal):
 1. (d x \<le> | y ] z) = (d x \<le> | d x * y ] z)
[PROOF STEP]
by auto


[STATEMENT]
lemma box_d_import_iff_2:
  "d(x) * d(y) \<le> |z]w \<longleftrightarrow> d(x) * d(y) \<le> |d(y) * z]w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * d y \<le> | z ] w) = (d x * d y \<le> | d y * z ] w)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d x * d y \<le> | z ] w \<Longrightarrow> d x * d y \<le> | d y * z ] w
 2. d x * d y \<le> | d y * z ] w \<Longrightarrow> d x * d y \<le> | z ] w
[PROOF STEP]
using box_d_export le_supI2
[PROOF STATE]
proof (prove)
using this:
| d ?x * ?y ] ?z = a ?x \<squnion> | ?y ] ?z
?x \<le> ?b \<Longrightarrow> ?x \<le> ?a \<squnion> ?b

goal (2 subgoals):
 1. d x * d y \<le> | z ] w \<Longrightarrow> d x * d y \<le> | d y * z ] w
 2. d x * d y \<le> | d y * z ] w \<Longrightarrow> d x * d y \<le> | z ] w
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * d y \<le> | d y * z ] w \<Longrightarrow> d x * d y \<le> | z ] w
[PROOF STEP]
by (metis box_d_import d_commutative d_restrict_iff_1)


[STATEMENT]
lemma box_demodalisation_2:
  "-p \<le> |y](-q) \<longleftrightarrow> -p * y * --q \<le> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a p \<le> | y ] a q) = (a p * y * a (a q) \<le> Z)
[PROOF STEP]
by (simp add: a_greatest_left_absorber box_def mult_assoc)


[STATEMENT]
lemma box_right_sub_dist_sup:
  "|x]d(y) \<squnion> |x]d(z) \<le> |x](d(y) \<squnion> d(z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] d y \<squnion> | x ] d z \<le> | x ] (d y \<squnion> d z)
[PROOF STEP]
by (simp add: box_right_isotone)


[STATEMENT]
lemma box_diff_var:
  "|x](d(y) \<squnion> a(z)) * |x]d(z) \<le> |x]d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] (d y \<squnion> a z) * | x ] d z \<le> | x ] d z
[PROOF STEP]
by (simp add: box_right_dist_sup box_x_d tests_dual.upper_bound_right)


[STATEMENT]
lemma diamond_demodalisation_2:
  "|x>y \<le> d(z) \<longleftrightarrow> a(z) * x * d(y) \<le> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (| x > y \<le> d z) = (a z * x * d y \<le> Z)
[PROOF STEP]
using a_antitone a_greatest_left_absorber a_mult_d d_def diamond_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> a ?y \<le> a ?x
(a ?x * ?y \<le> Z) = (a ?x \<le> a ?y)
a (?x * ?y) = a (?x * a (a ?y))
d ?x = a (a ?x)
| ?x > ?y = d (?x * ?y)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. (| x > y \<le> d z) = (a z * x * d y \<le> Z)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma box_below_Z:
  "( |x]y) * x * a(y) \<le> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x ] y * x * a y \<le> Z
[PROOF STEP]
by (simp add: a_restrict box_def mult_assoc)