[STATEMENT]
lemma finite_RPDs: "finite (RPDs r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RPDs r)
[PROOF STEP]
proof (induct r)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. finite (RPDs (MSkip x))
 2. \<And>x. finite (RPDs (MTestPos x))
 3. \<And>x. finite (RPDs (MTestNeg x))
 4. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 5. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 6. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
case MSkip
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. \<And>x. finite (RPDs (MSkip x))
 2. \<And>x. finite (RPDs (MTestPos x))
 3. \<And>x. finite (RPDs (MTestNeg x))
 4. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 5. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 6. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RPDs (MSkip x_))
[PROOF STEP]
by (intro finite_subset[OF RPDs_MSkip]) simp
[PROOF STATE]
proof (state)
this:
finite (RPDs (MSkip x_))

goal (5 subgoals):
 1. \<And>x. finite (RPDs (MTestPos x))
 2. \<And>x. finite (RPDs (MTestNeg x))
 3. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 4. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 5. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x. finite (RPDs (MTestPos x))
 2. \<And>x. finite (RPDs (MTestNeg x))
 3. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 4. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 5. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
case (MTestPos \<phi>)
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. \<And>x. finite (RPDs (MTestPos x))
 2. \<And>x. finite (RPDs (MTestNeg x))
 3. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 4. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 5. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RPDs (MTestPos \<phi>))
[PROOF STEP]
by (intro finite_subset[OF RPDs_Test(2)]) simp
[PROOF STATE]
proof (state)
this:
finite (RPDs (MTestPos \<phi>))

goal (4 subgoals):
 1. \<And>x. finite (RPDs (MTestNeg x))
 2. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 3. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 4. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. finite (RPDs (MTestNeg x))
 2. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 3. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 4. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
case (MTestNeg \<phi>)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>x. finite (RPDs (MTestNeg x))
 2. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 3. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 4. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RPDs (MTestNeg \<phi>))
[PROOF STEP]
by (intro finite_subset[OF RPDs_Test(3)]) simp
[PROOF STATE]
proof (state)
this:
finite (RPDs (MTestNeg \<phi>))

goal (3 subgoals):
 1. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 2. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 3. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 2. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 3. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
case (MPlus r s)
[PROOF STATE]
proof (state)
this:
finite (RPDs r)
finite (RPDs s)

goal (3 subgoals):
 1. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MPlus r1 r2))
 2. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 3. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (RPDs r)
finite (RPDs s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite (RPDs r)
finite (RPDs s)

goal (1 subgoal):
 1. finite (RPDs (MPlus r s))
[PROOF STEP]
by (intro finite_subset[OF RPDs_Plus]) simp
[PROOF STATE]
proof (state)
this:
finite (RPDs (MPlus r s))

goal (2 subgoals):
 1. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 2. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 2. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
case (MTimes r s)
[PROOF STATE]
proof (state)
this:
finite (RPDs r)
finite (RPDs s)

goal (2 subgoals):
 1. \<And>r1 r2. \<lbrakk>finite (RPDs r1); finite (RPDs r2)\<rbrakk> \<Longrightarrow> finite (RPDs (MTimes r1 r2))
 2. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (RPDs r)
finite (RPDs s)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite (RPDs r)
finite (RPDs s)

goal (1 subgoal):
 1. finite (RPDs (MTimes r s))
[PROOF STEP]
by (intro finite_subset[OF RPDs_Times]) (simp add: MTimesL_def)
[PROOF STATE]
proof (state)
this:
finite (RPDs (MTimes r s))

goal (1 subgoal):
 1. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
case (MStar r)
[PROOF STATE]
proof (state)
this:
finite (RPDs r)

goal (1 subgoal):
 1. \<And>r. finite (RPDs r) \<Longrightarrow> finite (RPDs (MStar r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (RPDs r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite (RPDs r)

goal (1 subgoal):
 1. finite (RPDs (MStar r))
[PROOF STEP]
by (intro finite_subset[OF RPDs_Star]) (simp add: MTimesL_def)
[PROOF STATE]
proof (state)
this:
finite (RPDs (MStar r))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_tuple_upd_None: "wf_tuple n A xs \<Longrightarrow> A - {i} = B \<Longrightarrow> wf_tuple n B (xs[i:=None])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_tuple n A xs; A - {i} = B\<rbrakk> \<Longrightarrow> wf_tuple n B (xs[i := None])
[PROOF STEP]
unfolding wf_tuple_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = n \<and> (\<forall>i<n. (xs ! i = None) = (i \<notin> A)); A - {i} = B\<rbrakk> \<Longrightarrow> length (xs[i := None]) = n \<and> (\<forall>ia<n. (xs[i := None] ! ia = None) = (ia \<notin> B))
[PROOF STEP]
by (auto simp: nth_list_update_alt)


[STATEMENT]
lemma mset_to_IP_closed:
  shows "set_mset m \<subseteq> I \<Longrightarrow>mset_to_IP R m \<in> indexed_pset I (carrier R) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset m \<subseteq> I \<Longrightarrow> mset_to_IP R m \<in> carrier R [\<X>\<^bsub>I\<^esub>]
[PROOF STEP]
apply(induction m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set_mset {#} \<subseteq> I \<Longrightarrow> mset_to_IP R {#} \<in> carrier R [\<X>\<^bsub>I\<^esub>]
 2. \<And>x m. \<lbrakk>set_mset m \<subseteq> I \<Longrightarrow> mset_to_IP R m \<in> carrier R [\<X>\<^bsub>I\<^esub>]; set_mset (add_mset x m) \<subseteq> I\<rbrakk> \<Longrightarrow> mset_to_IP R (add_mset x m) \<in> carrier R [\<X>\<^bsub>I\<^esub>]
[PROOF STEP]
apply (simp add: indexed_pset.indexed_const one_mset_to_IP)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x m. \<lbrakk>set_mset m \<subseteq> I \<Longrightarrow> mset_to_IP R m \<in> carrier R [\<X>\<^bsub>I\<^esub>]; set_mset (add_mset x m) \<subseteq> I\<rbrakk> \<Longrightarrow> mset_to_IP R (add_mset x m) \<in> carrier R [\<X>\<^bsub>I\<^esub>]
[PROOF STEP]
by (metis (no_types, lifting) add_mset_commute indexed_pset.simps
      monom_add_mset mset_add subset_iff union_single_eq_member)


[STATEMENT]
lemma Pring_zero:
"\<zero>\<^bsub>Pring R I\<^esub> = indexed_const \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero>\<^bsub>Pring R I\<^esub> = indexed_const \<zero>
[PROOF STEP]
unfolding Pring_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero>\<^bsub>\<lparr>carrier = carrier R [\<X>\<^bsub>I\<^esub>], monoid.mult = (\<Otimes>\<^sub>p), one = indexed_const \<one>, zero = indexed_const \<zero>, add = (\<Oplus>), smult = poly_scalar_mult R\<rparr>\<^esub> = indexed_const \<zero>
[PROOF STEP]
by simp


[STATEMENT]
lemma IP_to_UP_add:
  assumes " x \<in> carrier (Pring R {i})"
  assumes " y \<in> carrier (Pring R {i})"
  shows " IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) =
          IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) = IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) xa = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) xa
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) xa = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) xa
[PROOF STEP]
have LHS: "IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n)
[PROOF STEP]
by (meson IP_to_UP_def)
[PROOF STATE]
proof (state)
this:
IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n)

goal (1 subgoal):
 1. \<And>xa. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) xa = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n)
[PROOF STEP]
have LHS: "IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = x (nat_to_mset i n) \<oplus>\<^bsub>R\<^esub> y (nat_to_mset i n)"
[PROOF STATE]
proof (prove)
using this:
IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n)

goal (1 subgoal):
 1. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = x (nat_to_mset i n) \<oplus> y (nat_to_mset i n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n)
x \<in> carrier (Pring R {i})
y \<in> carrier (Pring R {i})

goal (1 subgoal):
 1. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = x (nat_to_mset i n) \<oplus> y (nat_to_mset i n)
[PROOF STEP]
unfolding IP_to_UP_def
[PROOF STATE]
proof (prove)
using this:
(x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n) = (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n)
x \<in> carrier (Pring R {i})
y \<in> carrier (Pring R {i})

goal (1 subgoal):
 1. (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) (nat_to_mset i n) = x (nat_to_mset i n) \<oplus> y (nat_to_mset i n)
[PROOF STEP]
by (metis R.Pring_add R.indexed_padd_def)
[PROOF STATE]
proof (state)
this:
IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = x (nat_to_mset i n) \<oplus> y (nat_to_mset i n)

goal (1 subgoal):
 1. \<And>xa. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) xa = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) xa
[PROOF STEP]
have RHS: "(IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n =
   (IP_to_UP i x) n \<oplus>\<^bsub>R\<^esub> (IP_to_UP i y) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n = IP_to_UP i x n \<oplus> IP_to_UP i y n
[PROOF STEP]
using assms UP_ring.cfs_add IP_to_UP_closed
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (Pring R {i})
y \<in> carrier (Pring R {i})
\<lbrakk>UP_ring ?R; ?p \<in> carrier (UP ?R); ?q \<in> carrier (UP ?R)\<rbrakk> \<Longrightarrow> (?p \<oplus>\<^bsub>UP ?R\<^esub> ?q) ?n = ?p ?n \<oplus>\<^bsub>?R\<^esub> ?q ?n
\<lbrakk>cring P; ?P \<in> carrier (Pring P {?i})\<rbrakk> \<Longrightarrow> IP_to_UP ?i ?P \<in> carrier (UP P)

goal (1 subgoal):
 1. (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n = IP_to_UP i x n \<oplus> IP_to_UP i y n
[PROOF STEP]
by (simp add: UP_ring.cfs_add R_cring cring.IP_to_UP_closed is_UP_ring)
[PROOF STATE]
proof (state)
this:
(IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n = IP_to_UP i x n \<oplus> IP_to_UP i y n

goal (1 subgoal):
 1. \<And>xa. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) xa = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) xa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n = IP_to_UP i x n \<oplus> IP_to_UP i y n
[PROOF STEP]
show "IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n"
[PROOF STATE]
proof (prove)
using this:
(IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n = IP_to_UP i x n \<oplus> IP_to_UP i y n

goal (1 subgoal):
 1. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n = IP_to_UP i x n \<oplus> IP_to_UP i y n
x \<in> carrier (Pring R {i})
y \<in> carrier (Pring R {i})

goal (1 subgoal):
 1. IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n
[PROOF STEP]
by (metis LHS IP_to_UP_def)
[PROOF STATE]
proof (state)
this:
IP_to_UP i (x \<oplus>\<^bsub>Pring R {i}\<^esub> y) n = (IP_to_UP i x \<oplus>\<^bsub>UP R\<^esub> IP_to_UP i y) n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aezdeltafun_decomp' :
  fixes b :: "'b::semiring_1"
  shows "b \<delta>\<delta> a = (1 \<delta>\<delta> a) * (b \<delta>\<delta> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<delta>\<delta> a = (1::'b) \<delta>\<delta> a * (b \<delta>\<delta> (0::'a))
[PROOF STEP]
using convolution_delta_delta[of 1 a b 0] deltafun_is_aezfun[of b 0]
        deltafun_is_aezfun[of 1 a] convolution_transfer
[PROOF STATE]
proof (prove)
using this:
convolution ((1::'b) \<delta> a) (b \<delta> (0::'a)) = ((1::'b) * b) \<delta> (a + (0::'a))
b \<delta> (0::?'c1) \<in> aezfun_set
(1::?'c1) \<delta> a \<in> aezfun_set
\<lbrakk>?f \<in> aezfun_set; ?g \<in> aezfun_set\<rbrakk> \<Longrightarrow> Abs_aezfun (convolution ?f ?g) = Abs_aezfun ?f * Abs_aezfun ?g

goal (1 subgoal):
 1. b \<delta>\<delta> a = (1::'b) \<delta>\<delta> a * (b \<delta>\<delta> (0::'a))
[PROOF STEP]
by    fastforce


[STATEMENT]
lemma (in RModule) Rmap_endomorph_is_RModuleEnd :
  assumes grpend: "GroupEnd M T"
  and     Rmap  : "\<And>r m. r \<in> R \<Longrightarrow> m \<in> M \<Longrightarrow> T (r \<cdot> m) = r \<cdot> (T m)"
  shows   "RModuleEnd R smult M T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RModuleEnd R (\<cdot>) M T
[PROOF STEP]
proof (rule RModuleEnd.intro, rule RModuleHomI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. GroupHom M T
 2. \<And>r m. \<lbrakk>r \<in> R; m \<in> M\<rbrakk> \<Longrightarrow> T (r \<cdot> m) = r \<cdot> T m
 3. RModuleEnd_axioms M T
[PROOF STEP]
from grpend
[PROOF STATE]
proof (chain)
picking this:
GroupEnd M T
[PROOF STEP]
show "GroupHom M T"
[PROOF STATE]
proof (prove)
using this:
GroupEnd M T

goal (1 subgoal):
 1. GroupHom M T
[PROOF STEP]
using GroupEnd.axioms(1)
[PROOF STATE]
proof (prove)
using this:
GroupEnd M T
GroupEnd ?G ?T \<Longrightarrow> GroupHom ?G ?T

goal (1 subgoal):
 1. GroupHom M T
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
GroupHom M T

goal (2 subgoals):
 1. \<And>r m. \<lbrakk>r \<in> R; m \<in> M\<rbrakk> \<Longrightarrow> T (r \<cdot> m) = r \<cdot> T m
 2. RModuleEnd_axioms M T
[PROOF STEP]
from grpend
[PROOF STATE]
proof (chain)
picking this:
GroupEnd M T
[PROOF STEP]
show "RModuleEnd_axioms M T"
[PROOF STATE]
proof (prove)
using this:
GroupEnd M T

goal (1 subgoal):
 1. RModuleEnd_axioms M T
[PROOF STEP]
using GroupEnd.endomorph
[PROOF STATE]
proof (prove)
using this:
GroupEnd M T
GroupEnd ?G ?T \<Longrightarrow> ?T ` ?G \<subseteq> ?G

goal (1 subgoal):
 1. RModuleEnd_axioms M T
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
RModuleEnd_axioms M T

goal (1 subgoal):
 1. \<And>r m. \<lbrakk>r \<in> R; m \<in> M\<rbrakk> \<Longrightarrow> T (r \<cdot> m) = r \<cdot> T m
[PROOF STEP]
qed (rule Rmap)


[STATEMENT]
lemma nth_aA_in_G [simp]: "i < card A \<Longrightarrow> aA!i \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < card A \<Longrightarrow> aA ! i \<in> G
[PROOF STEP]
using AsubG aA_def set_aA
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
aA \<equiv> list.map (from_nat_into A) [0..<card A]
set aA = A

goal (1 subgoal):
 1. i < card A \<Longrightarrow> aA ! i \<in> G
[PROOF STEP]
by auto


[STATEMENT]
lemma augmentum_dementum [simp]:
  assumes "0 \<notin> set ns" "sorted ns"
  shows "augmentum (dementum ns) = ns"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. augmentum (dementum ns) = ns
[PROOF STEP]
proof (rule nth_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (augmentum (dementum ns)) = length ns
 2. \<And>i. i < length (augmentum (dementum ns)) \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (augmentum (dementum ns)) = length ns
 2. \<And>i. i < length (augmentum (dementum ns)) \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
assume "i < length (augmentum (dementum ns))"
[PROOF STATE]
proof (state)
this:
i < length (augmentum (dementum ns))

goal (2 subgoals):
 1. length (augmentum (dementum ns)) = length ns
 2. \<And>i. i < length (augmentum (dementum ns)) \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (augmentum (dementum ns))
[PROOF STEP]
have i: "i < length ns"
[PROOF STATE]
proof (prove)
using this:
i < length (augmentum (dementum ns))

goal (1 subgoal):
 1. i < length ns
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < length ns

goal (2 subgoals):
 1. length (augmentum (dementum ns)) = length ns
 2. \<And>i. i < length (augmentum (dementum ns)) \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
show "augmentum (dementum ns)!i = ns!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
proof (cases "i=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
 2. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = 0

goal (2 subgoals):
 1. i = 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
 2. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 0

goal (1 subgoal):
 1. augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
using nth_augmentum dementum_def i
[PROOF STATE]
proof (prove)
using this:
i = 0
?i < length ?ns \<Longrightarrow> augmentum ?ns ! ?i = sum ((!) ?ns) {..?i}
dementum ?xs \<equiv> ?xs - (0 # ?xs)
i < length ns

goal (1 subgoal):
 1. augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
augmentum (dementum ns) ! i = ns ! i

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> 0

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have ns_le: "\<And>j. \<lbrakk>0 < j; j \<le> i\<rbrakk> \<Longrightarrow> ns ! (j - Suc 0) \<le> ns ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 < j; j \<le> i\<rbrakk> \<Longrightarrow> ns ! (j - Suc 0) \<le> ns ! j
[PROOF STEP]
using \<open>sorted ns\<close> i
[PROOF STATE]
proof (prove)
using this:
sorted ns
i < length ns

goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 < j; j \<le> i\<rbrakk> \<Longrightarrow> ns ! (j - Suc 0) \<le> ns ! j
[PROOF STEP]
by (simp add: sorted_iff_nth_mono)
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < ?j1; ?j1 \<le> i\<rbrakk> \<Longrightarrow> ns ! (?j1 - Suc 0) \<le> ns ! ?j1

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "augmentum (dementum ns)!i = (\<Sum>j\<le>i. ns!j - (if j = 0 then 0 else ns!(j-1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. augmentum (dementum ns) ! i = (\<Sum>j\<le>i. ns ! j - (if j = 0 then 0 else ns ! (j - 1)))
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length ns

goal (1 subgoal):
 1. augmentum (dementum ns) ! i = (\<Sum>j\<le>i. ns ! j - (if j = 0 then 0 else ns ! (j - 1)))
[PROOF STEP]
by (simp add: dementum_def nth_Cons')
[PROOF STATE]
proof (state)
this:
augmentum (dementum ns) ! i = (\<Sum>j\<le>i. ns ! j - (if j = 0 then 0 else ns ! (j - 1)))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
augmentum (dementum ns) ! i = (\<Sum>j\<le>i. ns ! j - (if j = 0 then 0 else ns ! (j - 1)))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "\<dots> = (\<Sum>j=0..i. if j = 0 then ns!0 else ns!j - ns!(j-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<le>i. ns ! j - (if j = 0 then 0 else ns ! (j - 1))) = (\<Sum>j = 0..i. if j = 0 then ns ! 0 else ns ! j - ns ! (j - 1))
[PROOF STEP]
by (smt (verit, best) diff_zero sum.cong atMost_atLeast0)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<le>i. ns ! j - (if j = 0 then 0 else ns ! (j - 1))) = (\<Sum>j = 0..i. if j = 0 then ns ! 0 else ns ! j - ns ! (j - 1))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<le>i. ns ! j - (if j = 0 then 0 else ns ! (j - 1))) = (\<Sum>j = 0..i. if j = 0 then ns ! 0 else ns ! j - ns ! (j - 1))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "\<dots> = ns!0 + (\<Sum>j\<in>{0<..i}. ns!j - ns!(j-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..i. if j = 0 then ns ! 0 else ns ! j - ns ! (j - 1)) = ns ! 0 + (\<Sum>j\<in>{0<..i}. ns ! j - ns ! (j - 1))
[PROOF STEP]
by (simp add: sum.head)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..i. if j = 0 then ns ! 0 else ns ! j - ns ! (j - 1)) = ns ! 0 + (\<Sum>j\<in>{0<..i}. ns ! j - ns ! (j - 1))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..i. if j = 0 then ns ! 0 else ns ! j - ns ! (j - 1)) = ns ! 0 + (\<Sum>j\<in>{0<..i}. ns ! j - ns ! (j - 1))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "\<dots> = ns!0 + ((\<Sum>j\<in>{0<..i}. ns!j) - (\<Sum>j\<in>{0<..i}. ns!(j-1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! 0 + (\<Sum>j\<in>{0<..i}. ns ! j - ns ! (j - 1)) = ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1)))
[PROOF STEP]
by (auto simp: ns_le intro: sum_subtractf_nat)
[PROOF STATE]
proof (state)
this:
ns ! 0 + (\<Sum>j\<in>{0<..i}. ns ! j - ns ! (j - 1)) = ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1)))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ns ! 0 + (\<Sum>j\<in>{0<..i}. ns ! j - ns ! (j - 1)) = ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1)))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "\<dots> = ns!0 + (\<Sum>j\<in>{0<..i}. ns!j) - (\<Sum>j\<in>{0<..i}. ns!(j-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))) = ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))) = ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))
[PROOF STEP]
have "(\<Sum>j\<in>{0<..i}. ns ! (j - 1)) \<le> sum ((!) ns) {0<..i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<in>{0<..i}. ns ! (j - 1)) \<le> sum ((!) ns) {0<..i}
[PROOF STEP]
by (metis One_nat_def greaterThanAtMost_iff ns_le sum_mono)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0<..i}. ns ! (j - 1)) \<le> sum ((!) ns) {0<..i}

goal (1 subgoal):
 1. ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))) = ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j\<in>{0<..i}. ns ! (j - 1)) \<le> sum ((!) ns) {0<..i}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j\<in>{0<..i}. ns ! (j - 1)) \<le> sum ((!) ns) {0<..i}

goal (1 subgoal):
 1. ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))) = ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))) = ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))) = ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ns ! 0 + (sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))) = ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1))

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "\<dots> = ns!0 + (\<Sum>j\<in>{0<..i}. ns!j) - (\<Sum>j\<le>i-Suc 0. ns!j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1)) = ns ! 0 + sum ((!) ns) {0<..i} - sum ((!) ns) {..i - Suc 0}
[PROOF STEP]
using sum.reindex [of Suc "{..i - Suc 0}" "\<lambda>j. ns!(j-1)", symmetric] False
[PROOF STATE]
proof (prove)
using this:
inj_on Suc {..i - Suc 0} \<Longrightarrow> sum ((\<lambda>j. ns ! (j - 1)) \<circ> Suc) {..i - Suc 0} = (\<Sum>j\<in>Suc ` {..i - Suc 0}. ns ! (j - 1))
i \<noteq> 0

goal (1 subgoal):
 1. ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1)) = ns ! 0 + sum ((!) ns) {0<..i} - sum ((!) ns) {..i - Suc 0}
[PROOF STEP]
by (simp add: image_Suc_atMost atLeastSucAtMost_greaterThanAtMost)
[PROOF STATE]
proof (state)
this:
ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1)) = ns ! 0 + sum ((!) ns) {0<..i} - sum ((!) ns) {..i - Suc 0}

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ns ! 0 + sum ((!) ns) {0<..i} - (\<Sum>j\<in>{0<..i}. ns ! (j - 1)) = ns ! 0 + sum ((!) ns) {0<..i} - sum ((!) ns) {..i - Suc 0}

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "\<dots> = (\<Sum>j=0..i. ns!j) - (\<Sum>j\<le>i-Suc 0. ns!j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ns ! 0 + sum ((!) ns) {0<..i} - sum ((!) ns) {..i - Suc 0} = sum ((!) ns) {0..i} - sum ((!) ns) {..i - Suc 0}
[PROOF STEP]
by (simp add:  sum.head [of 0 i])
[PROOF STATE]
proof (state)
this:
ns ! 0 + sum ((!) ns) {0<..i} - sum ((!) ns) {..i - Suc 0} = sum ((!) ns) {0..i} - sum ((!) ns) {..i - Suc 0}

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ns ! 0 + sum ((!) ns) {0<..i} - sum ((!) ns) {..i - Suc 0} = sum ((!) ns) {0..i} - sum ((!) ns) {..i - Suc 0}

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "\<dots> = (\<Sum>j=0..i-Suc 0. ns!j) + ns!i - (\<Sum>j\<le>i-Suc 0. ns!j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) ns) {0..i} - sum ((!) ns) {..i - Suc 0} = sum ((!) ns) {0..i - Suc 0} + ns ! i - sum ((!) ns) {..i - Suc 0}
[PROOF STEP]
by (metis False Suc_pred less_Suc0 not_less_eq sum.atLeast0_atMost_Suc)
[PROOF STATE]
proof (state)
this:
sum ((!) ns) {0..i} - sum ((!) ns) {..i - Suc 0} = sum ((!) ns) {0..i - Suc 0} + ns ! i - sum ((!) ns) {..i - Suc 0}

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum ((!) ns) {0..i} - sum ((!) ns) {..i - Suc 0} = sum ((!) ns) {0..i - Suc 0} + ns ! i - sum ((!) ns) {..i - Suc 0}

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
have "\<dots> = ns!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((!) ns) {0..i - Suc 0} + ns ! i - sum ((!) ns) {..i - Suc 0} = ns ! i
[PROOF STEP]
by (simp add: atLeast0AtMost)
[PROOF STATE]
proof (state)
this:
sum ((!) ns) {0..i - Suc 0} + ns ! i - sum ((!) ns) {..i - Suc 0} = ns ! i

goal (1 subgoal):
 1. i \<noteq> 0 \<Longrightarrow> augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
show "augmentum (dementum ns)!i = ns!i"
[PROOF STATE]
proof (prove)
using this:
augmentum (dementum ns) ! i = ns ! i

goal (1 subgoal):
 1. augmentum (dementum ns) ! i = ns ! i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
augmentum (dementum ns) ! i = ns ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
augmentum (dementum ns) ! i = ns ! i

goal (1 subgoal):
 1. length (augmentum (dementum ns)) = length ns
[PROOF STEP]
qed auto


[STATEMENT]
lemma verts_Gu: "uverts (G -- u) = uverts G - {u}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uverts (G -- u) = uverts G - {u}
[PROOF STEP]
unfolding remove_vertex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uverts (uverts G - {u}, uedges G - {A \<in> uedges G. u \<in> A}) = uverts G - {u}
[PROOF STEP]
by simp


[STATEMENT]
lemma embedded_meta_eq: "(A = B) \<Longrightarrow> (embedded_style A) = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B \<Longrightarrow> embedded_style A = B
[PROOF STEP]
unfolding embedded_style_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B \<Longrightarrow> id A = B
[PROOF STEP]
by auto


[STATEMENT]
lemma pick_index:
  assumes a: "a \<in> I" and a'_card: "a' < card I"
  shows "(pick I a' = a) = (index (sorted_list_of_set I) a = a')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
have finI: "finite I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite I
[PROOF STEP]
using a'_card card.infinite
[PROOF STATE]
proof (prove)
using this:
a' < card I
infinite ?A \<Longrightarrow> card ?A = 0

goal (1 subgoal):
 1. finite I
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
finite I

goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
have length_I: "length (sorted_list_of_set I) = card I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (sorted_list_of_set I) = card I
[PROOF STEP]
by (metis a'_card card.infinite distinct_card distinct_sorted_list_of_set
        not_less_zero set_sorted_list_of_set)
[PROOF STATE]
proof (state)
this:
length (sorted_list_of_set I) = card I

goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
let ?i = "index (sorted_list_of_set I) a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
have "(sorted_list_of_set I) ! a' = pick I a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set I ! a' = pick I a'
[PROOF STEP]
by (rule sorted_list_of_set_eq_pick, auto simp add: finI a'_card length_I)
[PROOF STATE]
proof (state)
this:
sorted_list_of_set I ! a' = pick I a'

goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted_list_of_set I ! a' = pick I a'

goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
have "(sorted_list_of_set I) ! ?i = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_list_of_set I ! index (sorted_list_of_set I) a = a
[PROOF STEP]
by (rule nth_index, simp add: a finI)
[PROOF STATE]
proof (state)
this:
sorted_list_of_set I ! index (sorted_list_of_set I) a = a

goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted_list_of_set I ! a' = pick I a'
sorted_list_of_set I ! index (sorted_list_of_set I) a = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sorted_list_of_set I ! a' = pick I a'
sorted_list_of_set I ! index (sorted_list_of_set I) a = a

goal (1 subgoal):
 1. (pick I a' = a) = (index (sorted_list_of_set I) a = a')
[PROOF STEP]
by (metis a'_card distinct_sorted_list_of_set index_nth_id length_I)
[PROOF STATE]
proof (state)
this:
(pick I a' = a) = (index (sorted_list_of_set I) a = a')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma InitNoneReds:
 "\<lbrakk> sh C = None;
    P \<turnstile> \<langle>INIT C' (C # Cs,False) \<leftarrow> e,(h, l, sh(C \<mapsto> (sblank P C, Prepared))),b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle> \<rbrakk>
\<Longrightarrow> P \<turnstile> \<langle>INIT C' (C#Cs,False) \<leftarrow> e,(h,l,sh),b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sh C = None; P \<turnstile> \<langle>INIT C' (C # Cs,False) \<leftarrow> e,(h, l, sh(C \<mapsto> (sblank P C, Prepared))),b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>INIT C' (C # Cs,False) \<leftarrow> e,(h, l, sh),b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sh C = None; P \<turnstile> \<langle>INIT C' (C # Cs,False) \<leftarrow> e,(h, l, sh(C \<mapsto> (sblank P C, Prepared))),b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>INIT C' (C # Cs,False) \<leftarrow> e,(h, l, sh),b\<rangle> \<rightarrow>* \<langle>e',s',b'\<rangle>
[PROOF STEP]
by(rule InitNoneRed[THEN converse_rtrancl_into_rtrancl])


[STATEMENT]
lemma "((A ** (B ** (C ** (D ** (E ** (F ** G)))))) imp (G ** (E ** (B ** (A ** (C ** (D ** F)))))))
  (h::'a::heap_sep_algebra)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<and>* B \<and>* C \<and>* D \<and>* E \<and>* F \<and>* G) h \<longrightarrow> (G \<and>* E \<and>* B \<and>* A \<and>* C \<and>* D \<and>* F) h
[PROOF STEP]
by separata


[STATEMENT]
lemma a''_calc: "$a''^{m}_n = (1 - $v^n) / $d^{m}" if "m \<noteq> 0" "i \<noteq> 0" for n m :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. $a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
have "$a''^{m}_n = (1+i).^(1/m) * ((1 - $v^n) / $i^{m})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. $a''^{m}_n = (1 + i) .^ (1 / real m) * ((1 - $v ^ n) / $i^{m})
[PROOF STEP]
using a''_a a_calc times_divide_eq_right that
[PROOF STATE]
proof (prove)
using this:
?m \<noteq> 0 \<Longrightarrow> $a''^{?m}_?n = (1 + i) .^ (1 / real ?m) * $a^{?m}_?n
\<lbrakk>?m \<noteq> 0; i \<noteq> 0\<rbrakk> \<Longrightarrow> $a^{?m}_?n = (1 - $v ^ ?n) / $i^{?m}
?a * (?b / ?c) = ?a * ?b / ?c
m \<noteq> 0
i \<noteq> 0

goal (1 subgoal):
 1. $a''^{m}_n = (1 + i) .^ (1 / real m) * ((1 - $v ^ n) / $i^{m})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
$a''^{m}_n = (1 + i) .^ (1 / real m) * ((1 - $v ^ n) / $i^{m})

goal (1 subgoal):
 1. $a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
$a''^{m}_n = (1 + i) .^ (1 / real m) * ((1 - $v ^ n) / $i^{m})

goal (1 subgoal):
 1. $a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
have "\<dots> = (1 - $v^n) / ($v.^(1/m) * $i^{m})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + i) .^ (1 / real m) * ((1 - $v ^ n) / $i^{m}) = (1 - $v ^ n) / ($v .^ (1 / real m) * $i^{m})
[PROOF STEP]
by (subst i_v, subst powr_powr, simp, subst powr_minus_divide, simp)
[PROOF STATE]
proof (state)
this:
(1 + i) .^ (1 / real m) * ((1 - $v ^ n) / $i^{m}) = (1 - $v ^ n) / ($v .^ (1 / real m) * $i^{m})

goal (1 subgoal):
 1. $a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 + i) .^ (1 / real m) * ((1 - $v ^ n) / $i^{m}) = (1 - $v ^ n) / ($v .^ (1 / real m) * $i^{m})

goal (1 subgoal):
 1. $a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
have "\<dots> = (1 - $v^n) / $d^{m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 - $v ^ n) / ($v .^ (1 / real m) * $i^{m}) = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
using d_nom_i_nom_v that
[PROOF STATE]
proof (prove)
using this:
?m \<noteq> 0 \<Longrightarrow> $d^{?m} = $i^{?m} * $v .^ (1 / real ?m)
m \<noteq> 0
i \<noteq> 0

goal (1 subgoal):
 1. (1 - $v ^ n) / ($v .^ (1 / real m) * $i^{m}) = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(1 - $v ^ n) / ($v .^ (1 / real m) * $i^{m}) = (1 - $v ^ n) / $d^{m}

goal (1 subgoal):
 1. $a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
$a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
$a''^{m}_n = (1 - $v ^ n) / $d^{m}

goal (1 subgoal):
 1. $a''^{m}_n = (1 - $v ^ n) / $d^{m}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
$a''^{m}_n = (1 - $v ^ n) / $d^{m}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fdomain_vsubset_VUnion2: "\<D>\<^sub>\<bullet> r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<bullet> r \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
assume "x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r
[PROOF STEP]
obtain y where "[x, y]\<^sub>\<circ> \<in>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r

goal (1 subgoal):
 1. (\<And>y. [x, y]\<^sub>\<circ> \<in>\<^sub>\<circ> r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[x, y]\<^sub>\<circ> \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x, y]\<^sub>\<circ> \<in>\<^sub>\<circ> r
[PROOF STEP]
have "set {\<langle>0\<^sub>\<nat>, x\<rangle>, \<langle>1\<^sub>\<nat>, y\<rangle>} \<in>\<^sub>\<circ> r"
[PROOF STATE]
proof (prove)
using this:
[x, y]\<^sub>\<circ> \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. set {\<langle>0\<^sub>\<nat>, x\<rangle>, \<langle>1\<^sub>\<nat>, y\<rangle>} \<in>\<^sub>\<circ> r
[PROOF STEP]
unfolding vcons_vdoubleton
[PROOF STATE]
proof (prove)
using this:
set {\<langle>0\<^sub>\<nat>, x\<rangle>, \<langle>1\<^sub>\<nat>, y\<rangle>} \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. set {\<langle>0\<^sub>\<nat>, x\<rangle>, \<langle>1\<^sub>\<nat>, y\<rangle>} \<in>\<^sub>\<circ> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set {\<langle>0\<^sub>\<nat>, x\<rangle>, \<langle>1\<^sub>\<nat>, y\<rangle>} \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
with insert_commute
[PROOF STATE]
proof (chain)
picking this:
insert ?x (insert ?y ?A) = insert ?y (insert ?x ?A)
set {\<langle>0\<^sub>\<nat>, x\<rangle>, \<langle>1\<^sub>\<nat>, y\<rangle>} \<in>\<^sub>\<circ> r
[PROOF STEP]
have "\<langle>0\<^sub>\<nat>, x\<rangle> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ>r"
[PROOF STATE]
proof (prove)
using this:
insert ?x (insert ?y ?A) = insert ?y (insert ?x ?A)
set {\<langle>0\<^sub>\<nat>, x\<rangle>, \<langle>1\<^sub>\<nat>, y\<rangle>} \<in>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<langle>0\<^sub>\<nat>, x\<rangle> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<langle>0\<^sub>\<nat>, x\<rangle> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> r

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<D>\<^sub>\<bullet> r \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>0\<^sub>\<nat>, x\<rangle> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> r
[PROOF STEP]
show "x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>(\<Union>\<^sub>\<circ>r))"
[PROOF STATE]
proof (prove)
using this:
\<langle>0\<^sub>\<nat>, x\<rangle> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> r

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
unfolding vpair_def
[PROOF STATE]
proof (prove)
using this:
set {set {0\<^sub>\<nat>}, set {0\<^sub>\<nat>, x}} \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> r

goal (1 subgoal):
 1. x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))
[PROOF STEP]
by (metis (full_types) VUnion_iff insert_commute vintersection_vdoubleton)
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> (\<Union>\<^sub>\<circ> r))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma frange_iff_vdomain: "b \<in>\<^sub>\<circ> \<R>\<^sub>\<bullet> r \<longleftrightarrow> (\<exists>a\<in>\<^sub>\<circ>\<D>\<^sub>\<bullet> r. [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<in>\<^sub>\<circ> \<R>\<^sub>\<bullet> r) = (\<exists>a\<in>elts (\<D>\<^sub>\<bullet> r). [a, b]\<^sub>\<circ> \<in>\<^sub>\<circ> r)
[PROOF STEP]
by auto


[STATEMENT]
lemma fimage_is_vempty[iff]: "r `\<^sub>\<bullet> A = 0 \<longleftrightarrow> vdisjnt (\<D>\<^sub>\<bullet> r) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r `\<^sub>\<bullet> A = []\<^sub>\<circ>) = (\<D>\<^sub>\<bullet> r \<inter>\<^sub>\<circ> A = []\<^sub>\<circ>)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma vote_set_upd:
  "vote_set (v_hist(r := v_f)) {p} =
      (if p \<in> dom v_f
        then insert (r, the (v_f p))
        else id
      )
      (if v_hist r p = None
        then vote_set v_hist {p}
        else vote_set v_hist {p} - {(r, the (v_hist r p))}
      )
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vote_set (v_hist(r := v_f)) {p} = (if p \<in> dom v_f then insert (r, the (v_f p)) else id) (if v_hist r p = None then vote_set v_hist {p} else vote_set v_hist {p} - {(r, the (v_hist r p))})
[PROOF STEP]
by(auto simp add: vote_set_def const_map_is_Some split: if_split_asm)


[STATEMENT]
lemma vote_setD:
  "rv \<in> vote_set v_f {a} \<Longrightarrow> v_f (fst rv) a = Some (snd rv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rv \<in> vote_set v_f {a} \<Longrightarrow> v_f (fst rv) a = Some (snd rv)
[PROOF STEP]
by(auto simp add: vote_set_def)


[STATEMENT]
lemma Hermite_of_row_i: "Hermite_of_row_i A i \<in> carrier_mat (dim_row A) (dim_col A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HNF_Mod_Det_Algorithm.Hermite_of_row_i A i \<in> carrier_mat (dim_row A) (dim_col A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HNF_Mod_Det_Algorithm.Hermite_of_row_i A i \<in> carrier_mat (dim_row A) (dim_col A)
[PROOF STEP]
have "Hermite_reduce_above (multrow i (- 1) A) i i a
    \<in> carrier_mat (dim_row (multrow i (- 1) A)) (dim_col (multrow i (- 1) A))"
    for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HNF_Mod_Det_Algorithm.Hermite_reduce_above (multrow i (- 1) A) i i a \<in> carrier_mat (dim_row (multrow i (- 1) A)) (dim_col (multrow i (- 1) A))
[PROOF STEP]
by (rule Hermite_reduce_above)
[PROOF STATE]
proof (state)
this:
HNF_Mod_Det_Algorithm.Hermite_reduce_above (multrow i (- 1) A) i i ?a \<in> carrier_mat (dim_row (multrow i (- 1) A)) (dim_col (multrow i (- 1) A))

goal (1 subgoal):
 1. HNF_Mod_Det_Algorithm.Hermite_of_row_i A i \<in> carrier_mat (dim_row A) (dim_col A)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
HNF_Mod_Det_Algorithm.Hermite_reduce_above (multrow i (- 1) A) i i ?a \<in> carrier_mat (dim_row (multrow i (- 1) A)) (dim_col (multrow i (- 1) A))

goal (1 subgoal):
 1. HNF_Mod_Det_Algorithm.Hermite_of_row_i A i \<in> carrier_mat (dim_row A) (dim_col A)
[PROOF STEP]
unfolding Hermite_of_row_i_def
[PROOF STATE]
proof (prove)
using this:
HNF_Mod_Det_Algorithm.Hermite_reduce_above (multrow i (- 1) A) i i ?a \<in> carrier_mat (dim_row (multrow i (- 1) A)) (dim_col (multrow i (- 1) A))

goal (1 subgoal):
 1. (case find_fst_non0_in_row i A of None \<Rightarrow> A | Some j \<Rightarrow> let Aij = A $$ (i, j) in if Aij < 0 then HNF_Mod_Det_Algorithm.Hermite_reduce_above (multrow i (- 1) A) i i j else HNF_Mod_Det_Algorithm.Hermite_reduce_above A i i j) \<in> carrier_mat (dim_row A) (dim_col A)
[PROOF STEP]
using Hermite_reduce_above
[PROOF STATE]
proof (prove)
using this:
HNF_Mod_Det_Algorithm.Hermite_reduce_above (multrow i (- 1) A) i i ?a \<in> carrier_mat (dim_row (multrow i (- 1) A)) (dim_col (multrow i (- 1) A))
HNF_Mod_Det_Algorithm.Hermite_reduce_above ?A ?n ?i ?j \<in> carrier_mat (dim_row ?A) (dim_col ?A)

goal (1 subgoal):
 1. (case find_fst_non0_in_row i A of None \<Rightarrow> A | Some j \<Rightarrow> let Aij = A $$ (i, j) in if Aij < 0 then HNF_Mod_Det_Algorithm.Hermite_reduce_above (multrow i (- 1) A) i i j else HNF_Mod_Det_Algorithm.Hermite_reduce_above A i i j) \<in> carrier_mat (dim_row A) (dim_col A)
[PROOF STEP]
by (cases "find_fst_non0_in_row i A", auto)
[PROOF STATE]
proof (state)
this:
HNF_Mod_Det_Algorithm.Hermite_of_row_i A i \<in> carrier_mat (dim_row A) (dim_col A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lem2: "N x \<longrightarrow> N(s(x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N x \<longrightarrow> N (s x)
[PROOF STEP]
by (simp add: N_def induct_def)


[STATEMENT]
lemma "map_head'_side xss \<longleftrightarrow> (\<forall>xs \<in> set xss. \<forall>x \<in> set xs. x \<noteq> [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_head'_side xss = (\<forall>xs\<in>set xss. \<forall>x\<in>set xs. x \<noteq> [])
[PROOF STEP]
by (auto intro: map_head'_side.intros elim: map_head'_side.cases)


[STATEMENT]
lemma sep_impl_sep_false[simp]:
  "(sep_false \<longrightarrow>\<^sup>* P) = sep_true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sep_false \<longrightarrow>\<^sup>* P) = sep_true
[PROOF STEP]
by (force intro!: sep_implI ext)


[STATEMENT]
lemma finer_ex:
assumes P: "part I0 P" and Q: "part I0 Q" and PQ: "finer P Q"
and I: "I \<in> P"
shows "\<exists> II. II \<in> Q \<and> I \<subseteq> II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
proof(cases "I = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. I = {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
 2. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
I = {}

goal (2 subgoals):
 1. I = {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
 2. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
have "Q \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<noteq> {}
[PROOF STEP]
using I PQ
[PROOF STATE]
proof (prove)
using this:
I \<in> P
finer P Q

goal (1 subgoal):
 1. Q \<noteq> {}
[PROOF STEP]
unfolding finer_def
[PROOF STATE]
proof (prove)
using this:
I \<in> P
(\<forall>J\<in>Q. J = \<Union> {I \<in> P. I \<subseteq> J}) \<and> (P \<noteq> {} \<longrightarrow> Q \<noteq> {})

goal (1 subgoal):
 1. Q \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q \<noteq> {}

goal (2 subgoals):
 1. I = {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
 2. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q \<noteq> {}
[PROOF STEP]
obtain JJ where "JJ \<in> Q"
[PROOF STATE]
proof (prove)
using this:
Q \<noteq> {}

goal (1 subgoal):
 1. (\<And>JJ. JJ \<in> Q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
JJ \<in> Q

goal (2 subgoals):
 1. I = {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
 2. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
I = {}
JJ \<in> Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
I = {}
JJ \<in> Q

goal (1 subgoal):
 1. \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>II. II \<in> Q \<and> I \<subseteq> II

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
I \<noteq> {}

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
I \<noteq> {}
[PROOF STEP]
obtain i where i: "i \<in> I"
[PROOF STATE]
proof (prove)
using this:
I \<noteq> {}

goal (1 subgoal):
 1. (\<And>i. i \<in> I \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> I

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
hence "i \<in> I0"
[PROOF STATE]
proof (prove)
using this:
i \<in> I

goal (1 subgoal):
 1. i \<in> I0
[PROOF STEP]
using I P
[PROOF STATE]
proof (prove)
using this:
i \<in> I
I \<in> P
part I0 P

goal (1 subgoal):
 1. i \<in> I0
[PROOF STEP]
unfolding part_def
[PROOF STATE]
proof (prove)
using this:
i \<in> I
I \<in> P
\<Union> P = I0 \<and> (\<forall>J1 J2. J1 \<in> P \<and> J2 \<in> P \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {})

goal (1 subgoal):
 1. i \<in> I0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> I0

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<in> I0
[PROOF STEP]
obtain II where II: "II \<in> Q" and "i \<in> II"
[PROOF STATE]
proof (prove)
using this:
i \<in> I0

goal (1 subgoal):
 1. (\<And>II. \<lbrakk>II \<in> Q; i \<in> II\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Q
[PROOF STATE]
proof (prove)
using this:
i \<in> I0
part I0 Q

goal (1 subgoal):
 1. (\<And>II. \<lbrakk>II \<in> Q; i \<in> II\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding part_def
[PROOF STATE]
proof (prove)
using this:
i \<in> I0
\<Union> Q = I0 \<and> (\<forall>J1 J2. J1 \<in> Q \<and> J2 \<in> Q \<and> J1 \<noteq> J2 \<longrightarrow> J1 \<inter> J2 = {})

goal (1 subgoal):
 1. (\<And>II. \<lbrakk>II \<in> Q; i \<in> II\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
II \<in> Q
i \<in> II

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
hence "I Int II \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
II \<in> Q
i \<in> II

goal (1 subgoal):
 1. I \<inter> II \<noteq> {}
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
II \<in> Q
i \<in> II
i \<in> I

goal (1 subgoal):
 1. I \<inter> II \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
I \<inter> II \<noteq> {}

goal (1 subgoal):
 1. I \<noteq> {} \<Longrightarrow> \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
I \<inter> II \<noteq> {}

goal (1 subgoal):
 1. \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
using assms I II finer_nchotomy[of I0 P Q I II]
[PROOF STATE]
proof (prove)
using this:
I \<inter> II \<noteq> {}
part I0 P
part I0 Q
finer P Q
I \<in> P
I \<in> P
II \<in> Q
\<lbrakk>part I0 P; part I0 Q; finer P Q; I \<in> P; II \<in> Q\<rbrakk> \<Longrightarrow> I \<subseteq> II \<or> I \<inter> II = {}

goal (1 subgoal):
 1. \<exists>II. II \<in> Q \<and> I \<subseteq> II
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>II. II \<in> Q \<and> I \<subseteq> II

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZObis_raw_coind:
assumes "theta \<le> ZOretr theta"
shows "theta \<le> ZObis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<subseteq> ZObis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. theta \<subseteq> ZObis
[PROOF STEP]
have "ZOretr theta \<subseteq> ZOretr (theta Un ZObis)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZOretr theta \<subseteq> ZOretr (theta \<union> ZObis)
[PROOF STEP]
by (metis Un_upper1 monoD mono_Retr)
[PROOF STATE]
proof (state)
this:
ZOretr theta \<subseteq> ZOretr (theta \<union> ZObis)

goal (1 subgoal):
 1. theta \<subseteq> ZObis
[PROOF STEP]
hence "theta \<subseteq> ZOretr (theta Un ZObis)"
[PROOF STATE]
proof (prove)
using this:
ZOretr theta \<subseteq> ZOretr (theta \<union> ZObis)

goal (1 subgoal):
 1. theta \<subseteq> ZOretr (theta \<union> ZObis)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ZOretr theta \<subseteq> ZOretr (theta \<union> ZObis)
theta \<subseteq> ZOretr theta

goal (1 subgoal):
 1. theta \<subseteq> ZOretr (theta \<union> ZObis)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
theta \<subseteq> ZOretr (theta \<union> ZObis)

goal (1 subgoal):
 1. theta \<subseteq> ZObis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> ZOretr (theta \<union> ZObis)

goal (1 subgoal):
 1. theta \<subseteq> ZObis
[PROOF STEP]
using ZObis_coind
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> ZOretr (theta \<union> ZObis)
?theta \<subseteq> ZOretr (?theta \<union> ZObis) \<Longrightarrow> ?theta \<subseteq> ZObis

goal (1 subgoal):
 1. theta \<subseteq> ZObis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
theta \<subseteq> ZObis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ZObisL_update[simp]:
assumes cldl: "ZObisL cl dl" and c'd': "c' \<approx>01 d'"
shows "ZObisL (cl [n := c']) (dl [n := d'])" (is "ZObisL ?cl' ?dl'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZObisL (cl[n := c']) (dl[n := d'])
[PROOF STEP]
proof(cases "n < length cl")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n < length cl \<Longrightarrow> ZObisL (cl[n := c']) (dl[n := d'])
 2. \<not> n < length cl \<Longrightarrow> ZObisL (cl[n := c']) (dl[n := d'])
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n < length cl

goal (2 subgoals):
 1. n < length cl \<Longrightarrow> ZObisL (cl[n := c']) (dl[n := d'])
 2. \<not> n < length cl \<Longrightarrow> ZObisL (cl[n := c']) (dl[n := d'])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZObisL (cl[n := c']) (dl[n := d'])
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (cl[n := c']) = length (dl[n := d'])
 2. \<And>na. \<lbrakk>na < length (cl[n := c']); na < length (dl[n := d'])\<rbrakk> \<Longrightarrow> cl[n := c'] ! na \<approx>01 dl[n := d'] ! na
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (cl[n := c']) = length (dl[n := d'])
 2. \<And>na. \<lbrakk>na < length (cl[n := c']); na < length (dl[n := d'])\<rbrakk> \<Longrightarrow> cl[n := c'] ! na \<approx>01 dl[n := d'] ! na
[PROOF STEP]
assume m: "m < length ?cl'" "m < length ?dl'"
[PROOF STATE]
proof (state)
this:
m < length (cl[n := c'])
m < length (dl[n := d'])

goal (2 subgoals):
 1. length (cl[n := c']) = length (dl[n := d'])
 2. \<And>na. \<lbrakk>na < length (cl[n := c']); na < length (dl[n := d'])\<rbrakk> \<Longrightarrow> cl[n := c'] ! na \<approx>01 dl[n := d'] ! na
[PROOF STEP]
thus "?cl' ! m \<approx>01 ?dl' ! m"
[PROOF STATE]
proof (prove)
using this:
m < length (cl[n := c'])
m < length (dl[n := d'])

goal (1 subgoal):
 1. cl[n := c'] ! m \<approx>01 dl[n := d'] ! m
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m < length (cl[n := c'])
m < length (dl[n := d'])
ZObisL cl dl
c' \<approx>01 d'

goal (1 subgoal):
 1. cl[n := c'] ! m \<approx>01 dl[n := d'] ! m
[PROOF STEP]
by (cases "m = n") auto
[PROOF STATE]
proof (state)
this:
cl[n := c'] ! m \<approx>01 dl[n := d'] ! m

goal (1 subgoal):
 1. length (cl[n := c']) = length (dl[n := d'])
[PROOF STEP]
qed (insert cldl, simp)
[PROOF STATE]
proof (state)
this:
ZObisL (cl[n := c']) (dl[n := d'])

goal (1 subgoal):
 1. \<not> n < length cl \<Longrightarrow> ZObisL (cl[n := c']) (dl[n := d'])
[PROOF STEP]
qed (insert cldl, simp)


[STATEMENT]
lemma fmdip_to_mip[rule_format]:
  "find_meth_def_in_path_f path m = Some ctxmd \<longrightarrow> m \<in> set (methods_in_path_f (map snd path))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_meth_def_in_path_f path m = Some ctxmd \<longrightarrow> m \<in> set (methods_in_path_f (map snd path))
[PROOF STEP]
apply(induct path)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. find_meth_def_in_path_f [] m = Some ctxmd \<longrightarrow> m \<in> set (methods_in_path_f (map snd []))
 2. \<And>a path. find_meth_def_in_path_f path m = Some ctxmd \<longrightarrow> m \<in> set (methods_in_path_f (map snd path)) \<Longrightarrow> find_meth_def_in_path_f (a # path) m = Some ctxmd \<longrightarrow> m \<in> set (methods_in_path_f (map snd (a # path)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path. find_meth_def_in_path_f path m = Some ctxmd \<longrightarrow> m \<in> set (methods_in_path_f (map snd path)) \<Longrightarrow> find_meth_def_in_path_f (a # path) m = Some ctxmd \<longrightarrow> m \<in> set (methods_in_path_f (map snd (a # path)))
[PROOF STEP]
apply(clarsimp simp add: class_methods_f_def split: option.splits cld.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path x2 x4. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, x2); find_meth_def_in_list_f x4 m = Some x2; ctxmd = (a, x2)\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set x4
[PROOF STEP]
apply(rename_tac aa bb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path aa bb. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, aa); find_meth_def_in_list_f bb m = Some aa; ctxmd = (a, aa)\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(case_tac aa)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path aa bb x1 x2. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, aa); find_meth_def_in_list_f bb m = Some aa; ctxmd = (a, aa); aa = meth_def_def x1 x2\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(rename_tac meth_sig meth_body)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path aa bb meth_sig meth_body. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, aa); find_meth_def_in_list_f bb m = Some aa; ctxmd = (a, aa); aa = meth_def_def meth_sig meth_body\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(case_tac meth_sig)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path aa bb meth_sig meth_body x1 x2 x3. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, aa); find_meth_def_in_list_f bb m = Some aa; ctxmd = (a, aa); aa = meth_def_def meth_sig meth_body; meth_sig = meth_sig_def x1 x2 x3\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path bb meth_body x1 x2 x3. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, meth_def_def (meth_sig_def x1 x2 x3) meth_body); find_meth_def_in_list_f bb m = Some (meth_def_def (meth_sig_def x1 x2 x3) meth_body); ctxmd = (a, meth_def_def (meth_sig_def x1 x2 x3) meth_body)\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(frule find_md_m_match')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path bb meth_body x1 x2 x3. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, meth_def_def (meth_sig_def x1 x2 x3) meth_body); find_meth_def_in_list_f bb m = Some (meth_def_def (meth_sig_def x1 x2 x3) meth_body); ctxmd = (a, meth_def_def (meth_sig_def x1 x2 x3) meth_body); x2 = m\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path bb meth_body x1 x3. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, meth_def_def (meth_sig_def x1 m x3) meth_body); find_meth_def_in_list_f bb m = Some (meth_def_def (meth_sig_def x1 m x3) meth_body); ctxmd = (a, meth_def_def (meth_sig_def x1 m x3) meth_body)\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(frule find_meth_def_in_list_mem)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path bb meth_body x1 x3. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, meth_def_def (meth_sig_def x1 m x3) meth_body); find_meth_def_in_list_f bb m = Some (meth_def_def (meth_sig_def x1 m x3) meth_body); ctxmd = (a, meth_def_def (meth_sig_def x1 m x3) meth_body); meth_def_def (meth_sig_def x1 m x3) meth_body \<in> set bb\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(frule m_image_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a path bb meth_body x1 x3. \<lbrakk>m \<notin> set (methods_in_path_f (map snd path)); find_meth_def_in_path_f path m \<noteq> Some (a, meth_def_def (meth_sig_def x1 m x3) meth_body); find_meth_def_in_list_f bb m = Some (meth_def_def (meth_sig_def x1 m x3) meth_body); ctxmd = (a, meth_def_def (meth_sig_def x1 m x3) meth_body); meth_def_def (meth_sig_def x1 m x3) meth_body \<in> set bb; m \<in> case_meth_def (\<lambda>meth_sig meth_body. case meth_sig of meth_sig_def cl meth vds \<Rightarrow> meth) ` set bb\<rbrakk> \<Longrightarrow> m \<in> (\<lambda>x. case x of meth_def_def (meth_sig_def cl meth vds) meth_body \<Rightarrow> meth) ` set bb
[PROOF STEP]
apply(assumption)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hermitian_mat_Ph:
  "hermitian mat_Ph"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hermitian mat_Ph
[PROOF STEP]
unfolding hermitian_def mat_Ph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint (mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0)) = mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0)
[PROOF STEP]
apply (rule eq_matI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0)); j < dim_col (mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0))\<rbrakk> \<Longrightarrow> adjoint (mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0)) $$ (i, j) = mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0) $$ (i, j)
 2. dim_row (adjoint (mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0))) = dim_row (mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0))
 3. dim_col (adjoint (mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0))) = dim_col (mat N N (\<lambda>(i, j). if i = j then if i = 0 then 1 else - 1 else 0))
[PROOF STEP]
by (auto simp add: adjoint_eval)


[STATEMENT]
lemma rtc_implies_cbelow_on:
  assumes "dw_closed A" and main: "a \<rightarrow>\<^sup>* b" and "a \<in> A" and "ord a c"
  shows "cbelow_on A ord c (\<leftrightarrow>) a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbelow_on A ord c (\<leftrightarrow>) a b
[PROOF STEP]
using main
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow>\<^sup>* b

goal (1 subgoal):
 1. cbelow_on A ord c (\<leftrightarrow>) a b
[PROOF STEP]
proof (induct rule: rtranclp_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cbelow_on A ord c (\<leftrightarrow>) a a
 2. \<And>y z. \<lbrakk>a \<rightarrow>\<^sup>* y; y \<rightarrow> z; cbelow_on A ord c (\<leftrightarrow>) a y\<rbrakk> \<Longrightarrow> cbelow_on A ord c (\<leftrightarrow>) a z
[PROOF STEP]
from assms(3) assms(4)
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
ord a c
[PROOF STEP]
show "cbelow_on A ord c (\<leftrightarrow>) a a"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
ord a c

goal (1 subgoal):
 1. cbelow_on A ord c (\<leftrightarrow>) a a
[PROOF STEP]
by (simp add: cbelow_on_def)
[PROOF STATE]
proof (state)
this:
cbelow_on A ord c (\<leftrightarrow>) a a

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>a \<rightarrow>\<^sup>* y; y \<rightarrow> z; cbelow_on A ord c (\<leftrightarrow>) a y\<rbrakk> \<Longrightarrow> cbelow_on A ord c (\<leftrightarrow>) a z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>a \<rightarrow>\<^sup>* y; y \<rightarrow> z; cbelow_on A ord c (\<leftrightarrow>) a y\<rbrakk> \<Longrightarrow> cbelow_on A ord c (\<leftrightarrow>) a z
[PROOF STEP]
fix b0 b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>a \<rightarrow>\<^sup>* y; y \<rightarrow> z; cbelow_on A ord c (\<leftrightarrow>) a y\<rbrakk> \<Longrightarrow> cbelow_on A ord c (\<leftrightarrow>) a z
[PROOF STEP]
assume "a \<rightarrow>\<^sup>* b0" and "b0 \<rightarrow> b" and IH: "cbelow_on A ord c (\<leftrightarrow>) a b0"
[PROOF STATE]
proof (state)
this:
a \<rightarrow>\<^sup>* b0
b0 \<rightarrow> b
cbelow_on A ord c (\<leftrightarrow>) a b0

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>a \<rightarrow>\<^sup>* y; y \<rightarrow> z; cbelow_on A ord c (\<leftrightarrow>) a y\<rbrakk> \<Longrightarrow> cbelow_on A ord c (\<leftrightarrow>) a z
[PROOF STEP]
from assms(1) assms(3) \<open>a \<rightarrow>\<^sup>* b0\<close>
[PROOF STATE]
proof (chain)
picking this:
dw_closed A
a \<in> A
a \<rightarrow>\<^sup>* b0
[PROOF STEP]
have "b0 \<in> A"
[PROOF STATE]
proof (prove)
using this:
dw_closed A
a \<in> A
a \<rightarrow>\<^sup>* b0

goal (1 subgoal):
 1. b0 \<in> A
[PROOF STEP]
by (rule dw_closed_rtrancl)
[PROOF STATE]
proof (state)
this:
b0 \<in> A

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>a \<rightarrow>\<^sup>* y; y \<rightarrow> z; cbelow_on A ord c (\<leftrightarrow>) a y\<rbrakk> \<Longrightarrow> cbelow_on A ord c (\<leftrightarrow>) a z
[PROOF STEP]
from assms(1) this \<open>b0 \<rightarrow> b\<close>
[PROOF STATE]
proof (chain)
picking this:
dw_closed A
b0 \<in> A
b0 \<rightarrow> b
[PROOF STEP]
have "b \<in> A"
[PROOF STATE]
proof (prove)
using this:
dw_closed A
b0 \<in> A
b0 \<rightarrow> b

goal (1 subgoal):
 1. b \<in> A
[PROOF STEP]
by (rule dw_closedD)
[PROOF STATE]
proof (state)
this:
b \<in> A

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>a \<rightarrow>\<^sup>* y; y \<rightarrow> z; cbelow_on A ord c (\<leftrightarrow>) a y\<rbrakk> \<Longrightarrow> cbelow_on A ord c (\<leftrightarrow>) a z
[PROOF STEP]
show "cbelow_on A ord c (\<leftrightarrow>) a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cbelow_on A ord c (\<leftrightarrow>) a b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. cbelow_on A ord c (\<leftrightarrow>) a ?b
 2. b \<in> A
 3. ?b \<leftrightarrow> b
 4. ord b c
[PROOF STEP]
from \<open>b0 \<rightarrow> b\<close>
[PROOF STATE]
proof (chain)
picking this:
b0 \<rightarrow> b
[PROOF STEP]
show "b0 \<leftrightarrow> b"
[PROOF STATE]
proof (prove)
using this:
b0 \<rightarrow> b

goal (1 subgoal):
 1. b0 \<leftrightarrow> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b0 \<leftrightarrow> b

goal (3 subgoals):
 1. cbelow_on A ord c (\<leftrightarrow>) a b0
 2. b \<in> A
 3. ord b c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. cbelow_on A ord c (\<leftrightarrow>) a b0
 2. b \<in> A
 3. ord b c
[PROOF STEP]
from relation_refines[OF \<open>b0 \<rightarrow> b\<close>] cbelow_on_second_below[OF IH]
[PROOF STATE]
proof (chain)
picking this:
ord b b0
ord b0 c
[PROOF STEP]
show "ord b c"
[PROOF STATE]
proof (prove)
using this:
ord b b0
ord b0 c

goal (1 subgoal):
 1. ord b c
[PROOF STEP]
by (rule trans)
[PROOF STATE]
proof (state)
this:
ord b c

goal (2 subgoals):
 1. cbelow_on A ord c (\<leftrightarrow>) a b0
 2. b \<in> A
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
cbelow_on A ord c (\<leftrightarrow>) a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "finite (nodes_of g - set ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes_of g - set ys)
[PROOF STEP]
proof(rule finite_subset)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. nodes_of g - set ys \<subseteq> ?B
 2. finite ?B
[PROOF STEP]
show "finite (nodes_of g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes_of g)
[PROOF STEP]
by (auto simp add: nodes_of_def)
[PROOF STATE]
proof (state)
this:
finite (nodes_of g)

goal (1 subgoal):
 1. nodes_of g - set ys \<subseteq> nodes_of g
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma smcf_comp_ObjMap_app[smc_cs_simps]:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and [simp]: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "(\<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
interpret L: is_semifunctor \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
interpret R: is_semifunctor \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
by
      (
        rule dghm_comp_ObjMap_app
          [
            OF L.smcf_is_dghm R.smcf_is_dghm,
            unfolded slicing_simps slicing_commute,
            OF assms(3)
          ]
      )
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smcf_comp_ArrMap_vrange:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>)\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret L: is_semifunctor \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret R: is_semifunctor \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by
      (
        rule dghm_comp_ArrMap_vrange
          [
            OF L.smcf_is_dghm R.smcf_is_dghm,
            unfolded slicing_simps slicing_commute
          ]
      )
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linord_of_list_sorted_on_subseqs:
  assumes "ys \<in> set (subseqs xs)"
  assumes "distinct xs"
  shows "sorted_on (linord_of_list (rev xs)) ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_on (linord_of_list (rev xs)) ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ys \<in> set (subseqs xs)
distinct xs

goal (1 subgoal):
 1. sorted_on (linord_of_list (rev xs)) ys
[PROOF STEP]
proof(induct ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>[] \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) []
 2. \<And>a ys. \<lbrakk>\<lbrakk>ys \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) ys; a # ys \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) (a # ys)
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>ys \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) ys
y # ys \<in> set (subseqs xs)
distinct xs

goal (2 subgoals):
 1. \<lbrakk>[] \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) []
 2. \<And>a ys. \<lbrakk>\<lbrakk>ys \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) ys; a # ys \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) (a # ys)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>ys \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) ys
y # ys \<in> set (subseqs xs)
distinct xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ys \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) ys
y # ys \<in> set (subseqs xs)
distinct xs

goal (1 subgoal):
 1. sorted_on (linord_of_list (rev xs)) (y # ys)
[PROOF STEP]
using linord_of_list_Linear_order[where xs="rev xs" and ys="Field (linord_of_list (rev xs))"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ys \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) ys
y # ys \<in> set (subseqs xs)
distinct xs
\<lbrakk>distinct (rev xs); Field (linord_of_list (rev xs)) = set (rev xs)\<rbrakk> \<Longrightarrow> Linear_order (linord_of_list (rev xs))

goal (1 subgoal):
 1. sorted_on (linord_of_list (rev xs)) (y # ys)
[PROOF STEP]
by (force simp: Cons_in_subseqsD sorted_on_Cons linord_of_list_linord_of_listP linord_of_listP_rev dest: subseqs_set)
[PROOF STATE]
proof (state)
this:
sorted_on (linord_of_list (rev xs)) (y # ys)

goal (1 subgoal):
 1. \<lbrakk>[] \<in> set (subseqs xs); distinct xs\<rbrakk> \<Longrightarrow> sorted_on (linord_of_list (rev xs)) []
[PROOF STEP]
qed simp


[STATEMENT]
lemma linear_order_on_list:
  assumes "linear_order_on ys r"
  assumes "ys = Field r"
  assumes "finite ys"
  shows "\<exists>!xs. r = linord_of_list xs \<and> distinct xs \<and> set xs = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!xs. r = linord_of_list xs \<and> distinct xs \<and> set xs = ys
[PROOF STEP]
using %invisible finite_sorted_on_distinct_unique[of r ys] sorted_on_linord_of_list[of r] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Linear_order r; ys \<subseteq> Field r; finite ys\<rbrakk> \<Longrightarrow> \<exists>!xs. set xs = ys \<and> sorted_on r xs \<and> distinct xs
\<lbrakk>Linear_order r; set ?xs = Field r; sorted_on r ?xs; distinct ?xs\<rbrakk> \<Longrightarrow> linord_of_list (rev ?xs) = r
linear_order_on ys r
ys = Field r
finite ys

goal (1 subgoal):
 1. \<exists>!xs. r = linord_of_list xs \<and> distinct xs \<and> set xs = ys
[PROOF STEP]
by simp (metis distinct_rev linord_of_list_sorted_on rev_rev_ident set_rev)


[STATEMENT]
lemma det_col_uminus: "det (upd_col M i (- a)) = - det (upd_col M i a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Square_Matrix.det (upd_col M i (- a)) = - Square_Matrix.det (upd_col M i a)
[PROOF STEP]
by (simp add: vector_sneg_minus1 det_col_mul)


[STATEMENT]
lemma wp_monty_switch_modular:
  "(\<lambda>s. 2/3) \<tturnstile> wp (monty True) \<guillemotleft>player_wins\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lambda>s. 2 / 3 \<tturnstile> wp (monty True) \<guillemotleft> player_wins \<guillemotright>
[PROOF STEP]
proof(rule wp_validD)  \<comment> \<open>Work in probabilistic Hoare triples\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
note wp_validI[OF wp_scale, OF wp_hide_prize, simplified]
    \<comment> \<open>Here we apply scaling to match our pre-expectation\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_def hide_prize; 0 \<le> ?c1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ?c1\<rbrace> hide_prize \<lbrace>\<lambda>s. ?c1 * \<guillemotleft> inv_prize \<guillemotright> s\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk>well_def hide_prize; 0 \<le> ?c1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ?c1\<rbrace> hide_prize \<lbrace>\<lambda>s. ?c1 * \<guillemotleft> inv_prize \<guillemotright> s\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
note wp_validI[OF wp_make_guess]
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>s. 2 / 3 * \<guillemotleft> inv_prize \<guillemotright> s\<rbrace> make_guess \<lbrace>\<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>s. 2 / 3 * \<guillemotleft> inv_prize \<guillemotright> s\<rbrace> make_guess \<lbrace>\<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
note wp_validI[OF wp_reveal]
[PROOF STATE]
proof (state)
this:
\<lbrace>\<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>\<rbrace> reveal \<lbrace>\<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrace>\<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>\<rbrace> reveal \<lbrace>\<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
note wp_validI[OF wp_switch_guess]
[PROOF STATE]
proof (state)
this:
\<lbrace>\<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>\<rbrace> switch_guess \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>well_def hide_prize; 0 \<le> 2 / 3; well_def hide_prize; well_def make_guess; sound (\<lambda>s. 2 / 3 * \<guillemotleft> inv_prize \<guillemotright> s); sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>; well_def (hide_prize ;; make_guess); well_def reveal; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>; well_def (hide_prize ;; make_guess ;; reveal); well_def switch_guess; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>; sound \<guillemotleft> player_wins \<guillemotright>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 2 / 3\<rbrace> hide_prize ;; make_guess ;; reveal ;; switch_guess \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
show "\<lbrace>\<lambda>s. 2/3\<rbrace> monty True \<lbrace>\<guillemotleft>player_wins\<guillemotright>\<rbrace>p"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_def hide_prize; 0 \<le> 2 / 3; well_def hide_prize; well_def make_guess; sound (\<lambda>s. 2 / 3 * \<guillemotleft> inv_prize \<guillemotright> s); sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>; well_def (hide_prize ;; make_guess); well_def reveal; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>; well_def (hide_prize ;; make_guess ;; reveal); well_def switch_guess; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>; sound \<guillemotleft> player_wins \<guillemotright>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 2 / 3\<rbrace> hide_prize ;; make_guess ;; reveal ;; switch_guess \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
unfolding monty_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>well_def hide_prize; 0 \<le> 2 / 3; well_def hide_prize; well_def make_guess; sound (\<lambda>s. 2 / 3 * \<guillemotleft> inv_prize \<guillemotright> s); sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>; well_def (hide_prize ;; make_guess); well_def reveal; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> inv_prize g \<and> inv_guess g \<guillemotright>; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>; well_def (hide_prize ;; make_guess ;; reveal); well_def switch_guess; sound \<guillemotleft> \<lambda>g. guess g \<noteq> prize g \<and> clue g \<noteq> prize g \<and> clue g \<noteq> guess g \<and> inv_prize g \<and> inv_guess g \<and> inv_clue g \<guillemotright>; sound \<guillemotleft> player_wins \<guillemotright>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. 2 / 3\<rbrace> hide_prize ;; make_guess ;; reveal ;; switch_guess \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 2 / 3\<rbrace> hide_prize ;; make_guess ;; reveal ;; (if True then switch_guess else Skip) \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p
[PROOF STEP]
by(simp add:wd_intros sound_intros monty_healthy)
[PROOF STATE]
proof (state)
this:
\<lbrace>\<lambda>s. 2 / 3\<rbrace> monty True \<lbrace>\<guillemotleft> player_wins \<guillemotright>\<rbrace>p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invar_var_goalI[vcg_comb_rules]:
    "invar_var_goal I R v s s'" if "\<paragraph>''Invar pres'' \<Longrightarrow> I s'" "\<paragraph>''Var pres'' \<Longrightarrow> (v s',v s)\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar_var_goal I R v s s'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<paragraph>''Invar pres'' \<Longrightarrow> I s'
\<paragraph>''Var pres'' \<Longrightarrow> (v s', v s) \<in> R

goal (1 subgoal):
 1. invar_var_goal I R v s s'
[PROOF STEP]
unfolding invar_var_goal_def GOAL_INDICATION_def
[PROOF STATE]
proof (prove)
using this:
True \<Longrightarrow> I s'
True \<Longrightarrow> (v s', v s) \<in> R

goal (1 subgoal):
 1. I s' \<and> (v s', v s) \<in> R
[PROOF STEP]
by auto


[STATEMENT]
lemma EndPhase1_HInv3:
  assumes act: "EndPhase1 s s' t"
  and     inv: "HInv3_inner s p q d"
  shows        "HInv3_inner s' p q d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv3_inner s' p q d
[PROOF STEP]
proof(cases "t=p \<or> t=q")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t = p \<or> t = q \<Longrightarrow> HInv3_inner s' p q d
 2. \<not> (t = p \<or> t = q) \<Longrightarrow> HInv3_inner s' p q d
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
t = p \<or> t = q

goal (2 subgoals):
 1. t = p \<or> t = q \<Longrightarrow> HInv3_inner s' p q d
 2. \<not> (t = p \<or> t = q) \<Longrightarrow> HInv3_inner s' p q d
[PROOF STEP]
with act inv
[PROOF STATE]
proof (chain)
picking this:
EndPhase1 s s' t
HInv3_inner s p q d
t = p \<or> t = q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
EndPhase1 s s' t
HInv3_inner s p q d
t = p \<or> t = q

goal (1 subgoal):
 1. HInv3_inner s' p q d
[PROOF STEP]
by(auto simp add: HInv3_inner_def
                dest: EndPhase1_HInv3_p EndPhase1_HInv3_q)
[PROOF STATE]
proof (state)
this:
HInv3_inner s' p q d

goal (1 subgoal):
 1. \<not> (t = p \<or> t = q) \<Longrightarrow> HInv3_inner s' p q d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (t = p \<or> t = q) \<Longrightarrow> HInv3_inner s' p q d
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (t = p \<or> t = q)

goal (1 subgoal):
 1. \<not> (t = p \<or> t = q) \<Longrightarrow> HInv3_inner s' p q d
[PROOF STEP]
with inv act
[PROOF STATE]
proof (chain)
picking this:
HInv3_inner s p q d
EndPhase1 s s' t
\<not> (t = p \<or> t = q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HInv3_inner s p q d
EndPhase1 s s' t
\<not> (t = p \<or> t = q)

goal (1 subgoal):
 1. HInv3_inner s' p q d
[PROOF STEP]
by(auto simp add: HInv3_inner_def dest: EndPhase1_HInv3_t)
[PROOF STATE]
proof (state)
this:
HInv3_inner s' p q d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma alw_ev_lockstep:
  assumes
    "alw (ev (holds P)) xs" "stream_all2 Q xs as"
    "\<And> x a. P x \<Longrightarrow> Q x a \<Longrightarrow> R a"
  shows
    "alw (ev (holds R)) as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. alw (ev (holds R)) as
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
alw (ev (holds P)) xs
stream_all2 Q xs as

goal (1 subgoal):
 1. alw (ev (holds R)) as
[PROOF STEP]
apply (coinduction arbitrary: xs as)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs as. \<lbrakk>alw (ev (holds P)) xs; stream_all2 Q xs as\<rbrakk> \<Longrightarrow> \<exists>xs. as = xs \<and> ev (holds R) xs \<and> ((\<exists>xsa as. stl xs = as \<and> alw (ev (holds P)) xsa \<and> stream_all2 Q xsa as) \<or> alw (ev (holds R)) (stl xs))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs as. \<lbrakk>alw (ev (holds P)) xs; stream_all2 Q xs as\<rbrakk> \<Longrightarrow> ev (holds R) as
 2. \<And>xs as. \<lbrakk>alw (ev (holds P)) xs; stream_all2 Q xs as; \<not> alw (ev (holds R)) as\<rbrakk> \<Longrightarrow> \<exists>xs. alw (ev (holds P)) xs \<and> stream_all2 Q xs (stl as)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (ev (holds P)) xs_; stream_all2 Q xs_ as_\<rbrakk> \<Longrightarrow> ev (holds R) as_
[PROOF STEP]
by (metis alw.cases assms(3) ev_holds_sset stream_all2_sset1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs as. \<lbrakk>alw (ev (holds P)) xs; stream_all2 Q xs as; \<not> alw (ev (holds R)) as\<rbrakk> \<Longrightarrow> \<exists>xs. alw (ev (holds P)) xs \<and> stream_all2 Q xs (stl as)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>alw (ev (holds P)) xs_; stream_all2 Q xs_ as_; \<not> alw (ev (holds R)) as_\<rbrakk> \<Longrightarrow> \<exists>xs. alw (ev (holds P)) xs \<and> stream_all2 Q xs (stl as_)
[PROOF STEP]
by (meson alw.cases stream.rel_sel)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mono_nest: "mono (nest r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (nest r)
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<subseteq> y \<longrightarrow> nest r x \<subseteq> nest r y
[PROOF STEP]
proof (intro allI impI subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa. \<lbrakk>x \<subseteq> y; xa \<in> nest r x\<rbrakk> \<Longrightarrow> xa \<in> nest r y
[PROOF STEP]
fix R S x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa. \<lbrakk>x \<subseteq> y; xa \<in> nest r x\<rbrakk> \<Longrightarrow> xa \<in> nest r y
[PROOF STEP]
assume 1: "R \<subseteq> S" and 2: "x \<in> nest r R"
[PROOF STATE]
proof (state)
this:
R \<subseteq> S
x \<in> nest r R

goal (1 subgoal):
 1. \<And>x y xa. \<lbrakk>x \<subseteq> y; xa \<in> nest r x\<rbrakk> \<Longrightarrow> xa \<in> nest r y
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
R \<subseteq> S
[PROOF STEP]
have "mult (letter_less r <*lex*> R) \<subseteq> mult (letter_less r <*lex*> S)"
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> S

goal (1 subgoal):
 1. mult (letter_less r <*lex*> R) \<subseteq> mult (letter_less r <*lex*> S)
[PROOF STEP]
using mono_mult mono_lex2[of "letter_less r"]
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> S
mono mult
mono ((<*lex*>) (letter_less r))

goal (1 subgoal):
 1. mult (letter_less r <*lex*> R) \<subseteq> mult (letter_less r <*lex*> S)
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
using this:
R \<subseteq> S
\<forall>x y. x \<subseteq> y \<longrightarrow> mult x \<subseteq> mult y
\<forall>x y. x \<subseteq> y \<longrightarrow> letter_less r <*lex*> x \<subseteq> letter_less r <*lex*> y

goal (1 subgoal):
 1. mult (letter_less r <*lex*> R) \<subseteq> mult (letter_less r <*lex*> S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
mult (letter_less r <*lex*> R) \<subseteq> mult (letter_less r <*lex*> S)

goal (1 subgoal):
 1. \<And>x y xa. \<lbrakk>x \<subseteq> y; xa \<in> nest r x\<rbrakk> \<Longrightarrow> xa \<in> nest r y
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
x \<in> nest r R
mult (letter_less r <*lex*> R) \<subseteq> mult (letter_less r <*lex*> S)
[PROOF STEP]
show "x \<in> nest r S"
[PROOF STATE]
proof (prove)
using this:
x \<in> nest r R
mult (letter_less r <*lex*> R) \<subseteq> mult (letter_less r <*lex*> S)

goal (1 subgoal):
 1. x \<in> nest r S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> nest r S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_greater_imp_not_empty:"n < length xs \<Longrightarrow> xs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> xs \<noteq> []
[PROOF STEP]
by fastforce


[STATEMENT]
lemma filter_snoc: "filter P (xs @ [x]) = (if P x then (filter P xs) @ [x] else filter P xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter P (xs @ [x]) = (if P x then filter P xs @ [x] else filter P xs)
[PROOF STEP]
by (case_tac "P x", simp+)


[STATEMENT]
lemma list_ord_Cons: "
  list_ord ord (x # xs) =
  (xs = [] \<or> (ord x (hd xs) \<and> list_ord ord xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_ord ord (x # xs) = (xs = [] \<or> ord x (hd xs) \<and> list_ord ord xs)
[PROOF STEP]
by (induct xs, simp+)