[STATEMENT]
lemma lunit_tensor_gen:
    assumes "ide a" and "ide b" and "ide c"
    shows "(a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
text\<open>
        We show that the lower right triangle in the following diagram commutes.
\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
text\<open>
$$\xymatrix{
  {@{term "((a \<otimes> \<I>) \<otimes> b) \<otimes> c"}}
     \ar[rrrr]^{\scriptsize @{term "\<a>[a, \<I>, b] \<otimes> c"}}
     \ar[ddd]_{\scriptsize @{term "\<a>[a \<otimes> \<I>, b, c]"}}
     \ar[drr]_{\scriptsize @{term "\<r>[a] \<otimes> b \<otimes> c"}}
  && &&
  {@{term "(a \<otimes> (\<I> \<otimes> b)) \<otimes> c"}}
     \ar[dll]^{\scriptsize @{term "(a \<otimes> \<l>[b]) \<otimes> c"}}
     \ar[ddd]^{\scriptsize @{term "\<a>[a, \<I> \<otimes> b, c]"}} \\
  && {@{term "(a \<otimes> b) \<otimes> c"}}
      \ar[d]^{\scriptsize @{term "\<a>[a, b, c]"}}    \\
  && {@{term "a \<otimes> b \<otimes> c"}}        \\
  {@{term "(a \<otimes> \<I>) \<otimes> b \<otimes> c"}}
      \ar[urr]^{\scriptsize @{term "\<r>[a] \<otimes> b \<otimes> c"}}
      \ar[drr]_{\scriptsize @{term "\<a>[a, \<I>, b \<otimes> c]"}}
  && &&
  {@{term "a \<otimes> (\<I> \<otimes> b) \<otimes> c"}}
      \ar[ull]_{\scriptsize @{term "a \<otimes> \<l>[b] \<otimes> c"}}
      \ar[dll]^{\scriptsize @{term "a \<otimes> \<a>[\<I>, b, c]"}}  \\
  && {@{term "a \<otimes> \<I> \<otimes> b \<otimes> c"}}
      \ar[uu]^{\scriptsize @{term "a \<otimes> \<l>[b \<otimes> c]"}}
}$$
\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
have "((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)) =
            ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c]
[PROOF STEP]
using assms pentagon comp_assoc
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide c
\<lbrakk>ide ?a; ide ?b; ide ?c; ide ?d\<rbrakk> \<Longrightarrow> (?a \<otimes> \<a>[?b, ?c, ?d]) \<cdot> \<a>[?a, ?b \<otimes> ?c, ?d] \<cdot> (\<a>[?a, ?b, ?c] \<otimes> ?d) = \<a>[?a, ?b, ?c \<otimes> ?d] \<cdot> \<a>[?a \<otimes> ?b, ?c, ?d]
(?h \<cdot> ?g) \<cdot> ?f = ?h \<cdot> ?g \<cdot> ?f

goal (1 subgoal):
 1. ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c]

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c]

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
have "... = (\<r>[a] \<otimes> (b \<otimes> c)) \<cdot> \<a>[a \<otimes> \<I>, b, c]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c] = (\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[a \<otimes> \<I>, b, c]
[PROOF STEP]
using assms triangle
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide c
\<lbrakk>ide ?a; ide ?b\<rbrakk> \<Longrightarrow> (?a \<otimes> \<l>[?b]) \<cdot> \<a>[?a, \<I>, ?b] = \<r>[?a] \<otimes> ?b

goal (1 subgoal):
 1. ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c] = (\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[a \<otimes> \<I>, b, c]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c] = (\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[a \<otimes> \<I>, b, c]

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> \<a>[a, \<I>, b \<otimes> c]) \<cdot> \<a>[a \<otimes> \<I>, b, c] = (\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[a \<otimes> \<I>, b, c]

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
have "... = \<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[a \<otimes> \<I>, b, c] = \<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c)
[PROOF STEP]
using assms assoc_naturality [of "\<r>[a]" b c]
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide c
\<lbrakk>arr \<r>[a]; arr b; arr c\<rbrakk> \<Longrightarrow> \<a>[cod \<r>[a], cod b, cod c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c) = (\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[local.dom \<r>[a], local.dom b, local.dom c]

goal (1 subgoal):
 1. (\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[a \<otimes> \<I>, b, c] = \<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[a \<otimes> \<I>, b, c] = \<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c)

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<r>[a] \<otimes> b \<otimes> c) \<cdot> \<a>[a \<otimes> \<I>, b, c] = \<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c)

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
have "... = (\<a>[a, b, c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c)) \<cdot> (\<a>[a, \<I>, b] \<otimes> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c) = (\<a>[a, b, c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c)) \<cdot> (\<a>[a, \<I>, b] \<otimes> c)
[PROOF STEP]
using assms triangle interchange comp_assoc
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide c
\<lbrakk>ide ?a; ide ?b\<rbrakk> \<Longrightarrow> (?a \<otimes> \<l>[?b]) \<cdot> \<a>[?a, \<I>, ?b] = \<r>[?a] \<otimes> ?b
\<lbrakk>seq ?h ?g; seq ?h' ?g'\<rbrakk> \<Longrightarrow> (?h \<otimes> ?h') \<cdot> (?g \<otimes> ?g') = ?h \<cdot> ?g \<otimes> ?h' \<cdot> ?g'
(?h \<cdot> ?g) \<cdot> ?f = ?h \<cdot> ?g \<cdot> ?f

goal (1 subgoal):
 1. \<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c) = (\<a>[a, b, c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c)) \<cdot> (\<a>[a, \<I>, b] \<otimes> c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c) = (\<a>[a, b, c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c)) \<cdot> (\<a>[a, \<I>, b] \<otimes> c)

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<a>[a, b, c] \<cdot> ((\<r>[a] \<otimes> b) \<otimes> c) = (\<a>[a, b, c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c)) \<cdot> (\<a>[a, \<I>, b] \<otimes> c)

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
have "... = (a \<otimes> (\<l>[b] \<otimes> c)) \<cdot> (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<a>[a, b, c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c)) \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)
[PROOF STEP]
using assms assoc_naturality [of a "\<l>[b]" c] comp_assoc
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide c
\<lbrakk>arr a; arr \<l>[b]; arr c\<rbrakk> \<Longrightarrow> \<a>[cod a, cod \<l>[b], cod c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[local.dom a, local.dom \<l>[b], local.dom c]
(?h \<cdot> ?g) \<cdot> ?f = ?h \<cdot> ?g \<cdot> ?f

goal (1 subgoal):
 1. (\<a>[a, b, c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c)) \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<a>[a, b, c] \<cdot> ((a \<otimes> \<l>[b]) \<otimes> c)) \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)
[PROOF STEP]
have 1: "((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)
                        = (a \<otimes> (\<l>[b] \<otimes> c)) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)"
[PROOF STATE]
proof (prove)
using this:
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)

goal (1 subgoal):
 1. ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
text\<open>
        The result follows by cancelling the isomorphism
        @{term "\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)"}
\<close>
[PROOF STATE]
proof (state)
this:
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
have 2: "iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
[PROOF STEP]
using assms isos_compose
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide c
\<lbrakk>local.iso ?f; local.iso ?f'; seq ?f' ?f\<rbrakk> \<Longrightarrow> local.iso (?f' \<cdot> ?f)

goal (1 subgoal):
 1. local.iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
have
          "seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide c

goal (1 subgoal):
 1. seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
have "seq (a \<otimes> (\<l>[b] \<otimes> c)) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. seq (a \<otimes> \<l>[b] \<otimes> c) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ide a
ide b
ide c

goal (1 subgoal):
 1. seq (a \<otimes> \<l>[b] \<otimes> c) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
seq (a \<otimes> \<l>[b] \<otimes> c) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
seq (a \<otimes> \<l>[b] \<otimes> c) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
seq (a \<otimes> \<l>[b] \<otimes> c) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
using 1 2 assms iso_is_retraction retraction_is_epi
              epiE [of "\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)"
                       "(a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])" "a \<otimes> \<l>[b] \<otimes> c"]
[PROOF STATE]
proof (prove)
using this:
local.iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
seq (a \<otimes> \<l>[b] \<otimes> c) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)
local.iso (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c))
ide a
ide b
ide c
local.iso ?f \<Longrightarrow> retraction ?f
retraction ?g \<Longrightarrow> epi ?g
\<lbrakk>epi (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)); seq ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)); seq (a \<otimes> \<l>[b] \<otimes> c) (\<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)); ((a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c])) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c) = (a \<otimes> \<l>[b] \<otimes> c) \<cdot> \<a>[a, \<I> \<otimes> b, c] \<cdot> (\<a>[a, \<I>, b] \<otimes> c)\<rbrakk> \<Longrightarrow> (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c

goal (1 subgoal):
 1. (a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a \<otimes> \<l>[b \<otimes> c]) \<cdot> (a \<otimes> \<a>[\<I>, b, c]) = a \<otimes> \<l>[b] \<otimes> c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<iota>_triangle:
    shows "\<iota> \<otimes> \<I> = (\<I> \<otimes> \<iota>) \<cdot> \<a>[\<I>, \<I>, \<I>]"
    and "(\<iota> \<otimes> \<I>) \<cdot> \<a>\<^sup>-\<^sup>1[\<I>, \<I>, \<I>] = \<I> \<otimes> \<iota>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<iota> \<otimes> \<I> = (\<I> \<otimes> \<iota>) \<cdot> \<a>[\<I>, \<I>, \<I>] &&& (\<iota> \<otimes> \<I>) \<cdot> \<a>\<^sup>-\<^sup>1[\<I>, \<I>, \<I>] = \<I> \<otimes> \<iota>
[PROOF STEP]
using triangle [of \<I> \<I>] triangle' [of \<I> \<I>] unitor_coincidence
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ide \<I>; ide \<I>\<rbrakk> \<Longrightarrow> (\<I> \<otimes> \<l>[\<I>]) \<cdot> \<a>[\<I>, \<I>, \<I>] = \<r>[\<I>] \<otimes> \<I>
\<lbrakk>ide \<I>; ide \<I>\<rbrakk> \<Longrightarrow> \<I> \<otimes> \<l>[\<I>] = (\<r>[\<I>] \<otimes> \<I>) \<cdot> \<a>\<^sup>-\<^sup>1[\<I>, \<I>, \<I>]
\<l>[\<I>] = \<iota>
\<r>[\<I>] = \<iota>

goal (1 subgoal):
 1. \<iota> \<otimes> \<I> = (\<I> \<otimes> \<iota>) \<cdot> \<a>[\<I>, \<I>, \<I>] &&& (\<iota> \<otimes> \<I>) \<cdot> \<a>\<^sup>-\<^sup>1[\<I>, \<I>, \<I>] = \<I> \<otimes> \<iota>
[PROOF STEP]
by auto


[STATEMENT]
lemma Diagonalize_preserves_Ide:
    assumes "Ide a"
    shows "Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>
[PROOF STEP]
have "Ide a \<Longrightarrow> Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ide a \<Longrightarrow> Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>
[PROOF STEP]
using Ide_implies_Arr TensorDiag_preserves_Ide Diag_Diagonalize
[PROOF STATE]
proof (prove)
using this:
Ide ?t \<Longrightarrow> Arr ?t
\<lbrakk>Ide ?t; Ide ?u; Diag ?t; Diag ?u\<rbrakk> \<Longrightarrow> Ide (?t \<^bold>\<lfloor>\<^bold>\<otimes>\<^bold>\<rfloor> ?u)
Arr ?t \<Longrightarrow> Diag \<^bold>\<lfloor>?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Dom \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Dom ?t\<^bold>\<rfloor>
Arr ?t \<Longrightarrow> Cod \<^bold>\<lfloor>?t\<^bold>\<rfloor> = \<^bold>\<lfloor>Cod ?t\<^bold>\<rfloor>

goal (1 subgoal):
 1. Ide a \<Longrightarrow> Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>
[PROOF STEP]
by (induct a) simp_all
[PROOF STATE]
proof (state)
this:
Ide a \<Longrightarrow> Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>

goal (1 subgoal):
 1. Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Ide a \<Longrightarrow> Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>

goal (1 subgoal):
 1. Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Ide a \<Longrightarrow> Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>
Ide a

goal (1 subgoal):
 1. Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Ide \<^bold>\<lfloor>a\<^bold>\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma load_not_cap_in_mem:
  assumes "tag c = True"
    and "perm_load c = True"
    and "offset c + |t|\<^sub>\<tau> \<le> base c + len c"
    and "offset c \<ge> base c"
    and "offset c mod |t|\<^sub>\<tau> = 0"
    and "Mapping.lookup (heap_map h) (block_id c) = Some (Map m)"
    and "offset c \<ge> fst (bounds m)"
    and "offset c + |t|\<^sub>\<tau> \<le> snd (bounds m)"
    and "\<not> is_contiguous_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>"
    and "\<not> is_cap (content m) (nat (offset c))"
  shows "load h c t = Success Undef"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. load h c t = Success Undef
[PROOF STEP]
unfolding load_def retrieve_tval_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if tag c = False then Error (C2Err TagViolation) else if perm_load c = False then Error (C2Err PermitLoadViolation) else if int (base c + len c) < offset c + int |t|\<^sub>\<tau> then Error (C2Err LengthViolation) else if offset c < int (base c) then Error (C2Err LengthViolation) else if offset c mod int |t|\<^sub>\<tau> \<noteq> 0 then Error (C2Err BadAddressViolation) else let obj = Mapping.lookup (heap_map h) (block_id c) in case obj of None \<Rightarrow> Error (LogicErr MissingResource) | Some Freed \<Rightarrow> Error (LogicErr UseAfterFree) | Some (Map m) \<Rightarrow> if offset c < int (fst (bounds m)) \<or> int (snd (bounds m)) < offset c + int |t|\<^sub>\<tau> then Error (LogicErr BufferOverrun) else Success (if is_contiguous_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau> then case t of Uint8 \<Rightarrow> Uint8_v (decode_u8_list (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Sint8 \<Rightarrow> Sint8_v (UCAST(8 \<rightarrow> 8 signed) (decode_u8_list (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>))) | Uint16 \<Rightarrow> Uint16_v (cat_u16 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Sint16 \<Rightarrow> Sint16_v (cat_s16 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Uint32 \<Rightarrow> Uint32_v (cat_u32 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Sint32 \<Rightarrow> Sint32_v (cat_s32 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Uint64 \<Rightarrow> Uint64_v (cat_u64 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Sint64 \<Rightarrow> Sint64_v (cat_s64 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Cap \<Rightarrow> if is_contiguous_zeros (content m) (nat (offset c)) |t|\<^sub>\<tau> then Cap_v NULL else Undef else if is_cap (content m) (nat (offset c)) then let cap = get_cap (content m) (nat (offset c)); tv = the (Mapping.lookup (tags m) (cap_offset (nat (offset c)))); ta = case perm_cap_load c of True \<Rightarrow> tv | False \<Rightarrow> False; cv = mem_capability.extend cap \<lparr>tag = ta\<rparr>; nth_frag = of_nth (the (Mapping.lookup (content m) (nat (offset c)))) in case t of Uint8 \<Rightarrow> Cap_v_frag (mem_capability.extend cap \<lparr>tag = False\<rparr>) nth_frag | Sint8 \<Rightarrow> Cap_v_frag (mem_capability.extend cap \<lparr>tag = False\<rparr>) nth_frag | Cap \<Rightarrow> if is_contiguous_cap (content m) cap (nat (offset c)) |t|\<^sub>\<tau> then Cap_v cv else Undef | _ \<Rightarrow> Undef else Undef)) = Success Undef
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
tag c = True
perm_load c = True
offset c + int |t|\<^sub>\<tau> \<le> int (base c + len c)
int (base c) \<le> offset c
offset c mod int |t|\<^sub>\<tau> = 0
Mapping.lookup (heap_map h) (block_id c) = Some (Map m)
int (fst (bounds m)) \<le> offset c
offset c + int |t|\<^sub>\<tau> \<le> int (snd (bounds m))
\<not> is_contiguous_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>
\<not> is_cap (content m) (nat (offset c))

goal (1 subgoal):
 1. (if tag c = False then Error (C2Err TagViolation) else if perm_load c = False then Error (C2Err PermitLoadViolation) else if int (base c + len c) < offset c + int |t|\<^sub>\<tau> then Error (C2Err LengthViolation) else if offset c < int (base c) then Error (C2Err LengthViolation) else if offset c mod int |t|\<^sub>\<tau> \<noteq> 0 then Error (C2Err BadAddressViolation) else let obj = Mapping.lookup (heap_map h) (block_id c) in case obj of None \<Rightarrow> Error (LogicErr MissingResource) | Some Freed \<Rightarrow> Error (LogicErr UseAfterFree) | Some (Map m) \<Rightarrow> if offset c < int (fst (bounds m)) \<or> int (snd (bounds m)) < offset c + int |t|\<^sub>\<tau> then Error (LogicErr BufferOverrun) else Success (if is_contiguous_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau> then case t of Uint8 \<Rightarrow> Uint8_v (decode_u8_list (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Sint8 \<Rightarrow> Sint8_v (UCAST(8 \<rightarrow> 8 signed) (decode_u8_list (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>))) | Uint16 \<Rightarrow> Uint16_v (cat_u16 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Sint16 \<Rightarrow> Sint16_v (cat_s16 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Uint32 \<Rightarrow> Uint32_v (cat_u32 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Sint32 \<Rightarrow> Sint32_v (cat_s32 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Uint64 \<Rightarrow> Uint64_v (cat_u64 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Sint64 \<Rightarrow> Sint64_v (cat_s64 (retrieve_bytes (content m) (nat (offset c)) |t|\<^sub>\<tau>)) | Cap \<Rightarrow> if is_contiguous_zeros (content m) (nat (offset c)) |t|\<^sub>\<tau> then Cap_v NULL else Undef else if is_cap (content m) (nat (offset c)) then let cap = get_cap (content m) (nat (offset c)); tv = the (Mapping.lookup (tags m) (cap_offset (nat (offset c)))); ta = case perm_cap_load c of True \<Rightarrow> tv | False \<Rightarrow> False; cv = mem_capability.extend cap \<lparr>tag = ta\<rparr>; nth_frag = of_nth (the (Mapping.lookup (content m) (nat (offset c)))) in case t of Uint8 \<Rightarrow> Cap_v_frag (mem_capability.extend cap \<lparr>tag = False\<rparr>) nth_frag | Sint8 \<Rightarrow> Cap_v_frag (mem_capability.extend cap \<lparr>tag = False\<rparr>) nth_frag | Cap \<Rightarrow> if is_contiguous_cap (content m) cap (nat (offset c)) |t|\<^sub>\<tau> then Cap_v cv else Undef | _ \<Rightarrow> Undef else Undef)) = Success Undef
[PROOF STEP]
by fastforce


[STATEMENT]
lemma PO_m1a_obs_secrecy [iff]: "oreach m1a \<subseteq> m1x_secrecy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oreach m1a \<subseteq> m1x_secrecy
[PROOF STEP]
apply (rule_tac Q=m1x_secrecy in external_invariant_translation)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. oreach ?Sa \<subseteq> m1x_secrecy
 2. ?pi -` m1x_secrecy \<subseteq> m1x_secrecy
 3. implements ?pi ?Sa m1a
[PROOF STEP]
apply (auto del: subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. med1x1a -` m1x_secrecy \<subseteq> m1x_secrecy
[PROOF STEP]
apply (auto simp add: med1x1a_def m1x_secrecy_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1a_step4_refines_a0_rs_skip:
  "{R_a0m1a_rs}
     Id, (m1a_step4 Ra A B Na Kab nla)
   {> R_a0m1a_rs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0m1a_rs} Id, m1a_step4 Ra A B Na Kab nla {> R_a0m1a_rs}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R_a0m1a_rs_defs a0i_defs m1a_defs)


[STATEMENT]
lemma quasinorm_intersection:
  "eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f"
  "defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f &&& defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f
 2. defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2)
[PROOF STEP]
have T: "eNorm N1 (x + y) + eNorm N2 (x + y) \<le>
    ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
[PROOF STEP]
have "eNorm N1 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N1 x + ennreal (max (defect N1) (defect N2)) * eNorm N1 y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm N1 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N1 x + ennreal (max (defect N1) (defect N2)) * eNorm N1 y
[PROOF STEP]
using eNorm_triangular_ineq[of N1 x y]
[PROOF STATE]
proof (prove)
using this:
eNorm N1 (x + y) \<le> ennreal (defect N1) * eNorm N1 x + ennreal (defect N1) * eNorm N1 y

goal (1 subgoal):
 1. eNorm N1 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N1 x + ennreal (max (defect N1) (defect N2)) * eNorm N1 y
[PROOF STEP]
by (metis (no_types) max_def distrib_left ennreal_leI mult_right_mono order_trans zero_le)
[PROOF STATE]
proof (state)
this:
eNorm N1 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N1 x + ennreal (max (defect N1) (defect N2)) * eNorm N1 y

goal (1 subgoal):
 1. eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eNorm N1 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N1 x + ennreal (max (defect N1) (defect N2)) * eNorm N1 y

goal (1 subgoal):
 1. eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
[PROOF STEP]
have "eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N2 x + ennreal (max (defect N1) (defect N2)) * eNorm N2 y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N2 x + ennreal (max (defect N1) (defect N2)) * eNorm N2 y
[PROOF STEP]
using eNorm_triangular_ineq[of N2 x y]
[PROOF STATE]
proof (prove)
using this:
eNorm N2 (x + y) \<le> ennreal (defect N2) * eNorm N2 x + ennreal (defect N2) * eNorm N2 y

goal (1 subgoal):
 1. eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N2 x + ennreal (max (defect N1) (defect N2)) * eNorm N2 y
[PROOF STEP]
by (metis (no_types) max_def max.commute distrib_left ennreal_leI mult_right_mono order_trans zero_le)
[PROOF STATE]
proof (state)
this:
eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N2 x + ennreal (max (defect N1) (defect N2)) * eNorm N2 y

goal (1 subgoal):
 1. eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eNorm N1 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N1 x + ennreal (max (defect N1) (defect N2)) * eNorm N1 y
eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N2 x + ennreal (max (defect N1) (defect N2)) * eNorm N2 y
[PROOF STEP]
have "eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N1 y + (eNorm N2 x + eNorm N2 y))"
[PROOF STATE]
proof (prove)
using this:
eNorm N1 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N1 x + ennreal (max (defect N1) (defect N2)) * eNorm N1 y
eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * eNorm N2 x + ennreal (max (defect N1) (defect N2)) * eNorm N2 y

goal (1 subgoal):
 1. eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N1 y + (eNorm N2 x + eNorm N2 y))
[PROOF STEP]
by (simp add: add_mono_thms_linordered_semiring(1) distrib_left)
[PROOF STATE]
proof (state)
this:
eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N1 y + (eNorm N2 x + eNorm N2 y))

goal (1 subgoal):
 1. eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N1 y + (eNorm N2 x + eNorm N2 y))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N1 y + (eNorm N2 x + eNorm N2 y))

goal (1 subgoal):
 1. eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
[PROOF STEP]
by (simp add: ab_semigroup_add_class.add_ac(1) add.left_commute distrib_left)
[PROOF STATE]
proof (state)
this:
eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eNorm N1 (?x + ?y) + eNorm N2 (?x + ?y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 ?x + eNorm N2 ?x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 ?y + eNorm N2 ?y)

goal (2 subgoals):
 1. eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f
 2. defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2)
[PROOF STEP]
have H: "eNorm N1 (c *\<^sub>R x) + eNorm N2 (c *\<^sub>R x) \<le> ennreal \<bar>c\<bar> * (eNorm N1 x + eNorm N2 x)" for c x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eNorm N1 (c *\<^sub>R x) + eNorm N2 (c *\<^sub>R x) \<le> ennreal \<bar>c\<bar> * (eNorm N1 x + eNorm N2 x)
[PROOF STEP]
by (simp add: eNorm_cmult[of N1 c x] eNorm_cmult[of N2 c x] distrib_left)
[PROOF STATE]
proof (state)
this:
eNorm N1 (?c *\<^sub>R ?x) + eNorm N2 (?c *\<^sub>R ?x) \<le> ennreal \<bar>?c\<bar> * (eNorm N1 ?x + eNorm N2 ?x)

goal (2 subgoals):
 1. eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f
 2. defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2)
[PROOF STEP]
have *: "quasinorm_on UNIV (max (defect N1) (defect N2)) (\<lambda>f. eNorm N1 f + eNorm N2 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quasinorm_on UNIV (max (defect N1) (defect N2)) (\<lambda>f. eNorm N1 f + eNorm N2 f)
[PROOF STEP]
apply (rule quasinorm_onI)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> x + y \<in> UNIV
 2. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> UNIV\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> UNIV
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> UNIV\<rbrakk> \<Longrightarrow> eNorm N1 (c *\<^sub>R x) + eNorm N2 (c *\<^sub>R x) \<le> ennreal \<bar>c\<bar> * (eNorm N1 x + eNorm N2 x)
 5. (0::'a) \<in> UNIV
 6. eNorm N1 (0::'a) + eNorm N2 (0::'a) = 0
 7. 1 \<le> max (defect N1) (defect N2)
[PROOF STEP]
using T H defect_ge_1[of N1] defect_ge_1[of N2]
[PROOF STATE]
proof (prove)
using this:
eNorm N1 (?x + ?y) + eNorm N2 (?x + ?y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 ?x + eNorm N2 ?x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 ?y + eNorm N2 ?y)
eNorm N1 (?c *\<^sub>R ?x) + eNorm N2 (?c *\<^sub>R ?x) \<le> ennreal \<bar>?c\<bar> * (eNorm N1 ?x + eNorm N2 ?x)
1 \<le> defect N1
1 \<le> defect N2

goal (7 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> x + y \<in> UNIV
 2. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> eNorm N1 (x + y) + eNorm N2 (x + y) \<le> ennreal (max (defect N1) (defect N2)) * (eNorm N1 x + eNorm N2 x) + ennreal (max (defect N1) (defect N2)) * (eNorm N1 y + eNorm N2 y)
 3. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> UNIV\<rbrakk> \<Longrightarrow> c *\<^sub>R x \<in> UNIV
 4. \<And>c x. \<lbrakk>c \<noteq> 0; x \<in> UNIV\<rbrakk> \<Longrightarrow> eNorm N1 (c *\<^sub>R x) + eNorm N2 (c *\<^sub>R x) \<le> ennreal \<bar>c\<bar> * (eNorm N1 x + eNorm N2 x)
 5. (0::'a) \<in> UNIV
 6. eNorm N1 (0::'a) + eNorm N2 (0::'a) = 0
 7. 1 \<le> max (defect N1) (defect N2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
quasinorm_on UNIV (max (defect N1) (defect N2)) (\<lambda>f. eNorm N1 f + eNorm N2 f)

goal (2 subgoals):
 1. eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f
 2. defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2)
[PROOF STEP]
show "defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2)"
       "eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2) &&& eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f
[PROOF STEP]
unfolding quasinorm_intersection_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. defect (quasinorm_of (max (defect N1) (defect N2), \<lambda>f. eNorm N1 f + eNorm N2 f)) = max (defect N1) (defect N2) &&& eNorm (quasinorm_of (max (defect N1) (defect N2), \<lambda>f. eNorm N1 f + eNorm N2 f)) f = eNorm N1 f + eNorm N2 f
[PROOF STEP]
using quasinorm_of[OF *]
[PROOF STATE]
proof (prove)
using this:
eNorm (quasinorm_of (max (defect N1) (defect N2), \<lambda>f. eNorm N1 f + eNorm N2 f)) ?x = eNorm N1 ?x + eNorm N2 ?x
defect (quasinorm_of (max (defect N1) (defect N2), \<lambda>f. eNorm N1 f + eNorm N2 f)) = max (defect N1) (defect N2)

goal (1 subgoal):
 1. defect (quasinorm_of (max (defect N1) (defect N2), \<lambda>f. eNorm N1 f + eNorm N2 f)) = max (defect N1) (defect N2) &&& eNorm (quasinorm_of (max (defect N1) (defect N2), \<lambda>f. eNorm N1 f + eNorm N2 f)) f = eNorm N1 f + eNorm N2 f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
defect (N1 \<inter>\<^sub>N N2) = max (defect N1) (defect N2)
eNorm (N1 \<inter>\<^sub>N N2) f = eNorm N1 f + eNorm N2 f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_stabiliser: "tetrahedral.stabiliser A = stabiliser_A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tetrahedral.stabiliser A = stabiliser_A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. tetrahedral.stabiliser A \<subseteq> stabiliser_A
 2. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
show "stabiliser_A \<subseteq> tetrahedral.stabiliser A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
have "id \<in> complex_rotations"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id \<in> complex_rotations
[PROOF STEP]
using complex_rotations.intros simple_rotations_def
[PROOF STATE]
proof (prove)
using this:
?r \<in> simple_rotations \<Longrightarrow> ?r \<in> complex_rotations
\<lbrakk>?r \<in> simple_rotations; ?s \<in> complex_rotations\<rbrakk> \<Longrightarrow> ?r \<circ> ?s \<in> complex_rotations
simple_rotations = {id, rotate_A, rotate_B, rotate_C, rotate_D}

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

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
id \<in> complex_rotations
[PROOF STEP]
have "id \<in> carrier tetrahedral_group"
[PROOF STATE]
proof (prove)
using this:
id \<in> complex_rotations

goal (1 subgoal):
 1. id \<in> carrier tetrahedral_group
[PROOF STEP]
unfolding tetrahedral_group_def partial_object.select_convs(1)
[PROOF STATE]
proof (prove)
using this:
id \<in> complex_rotations

goal (1 subgoal):
 1. id \<in> complex_rotations
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
id \<in> carrier tetrahedral_group

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
id \<in> carrier tetrahedral_group

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
have "apply_rotation id A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_rotation id A = A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_rotation id A = A

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
id \<in> carrier tetrahedral_group
apply_rotation id A = A
[PROOF STEP]
have id:"id \<in> (tetrahedral.stabiliser A)"
[PROOF STATE]
proof (prove)
using this:
id \<in> carrier tetrahedral_group
apply_rotation id A = A

goal (1 subgoal):
 1. id \<in> tetrahedral.stabiliser A
[PROOF STEP]
using tetrahedral.stabiliser_def mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
id \<in> carrier tetrahedral_group
apply_rotation id A = A
tetrahedral.stabiliser ?x = {g \<in> carrier tetrahedral_group. apply_rotation g ?x = ?x}
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. id \<in> tetrahedral.stabiliser A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
id \<in> tetrahedral.stabiliser A

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
have "rotate_A \<in> simple_rotations"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotate_A \<in> simple_rotations
[PROOF STEP]
using simple_rotations_def insert_subset subset_insertI
[PROOF STATE]
proof (prove)
using this:
simple_rotations = {id, rotate_A, rotate_B, rotate_C, rotate_D}
(insert ?x ?A \<subseteq> ?B) = (?x \<in> ?B \<and> ?A \<subseteq> ?B)
?B \<subseteq> insert ?a ?B

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

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rotate_A \<in> simple_rotations
[PROOF STEP]
have "rotate_A \<in> complex_rotations"
[PROOF STATE]
proof (prove)
using this:
rotate_A \<in> simple_rotations

goal (1 subgoal):
 1. rotate_A \<in> complex_rotations
[PROOF STEP]
using complex_rotations.intros(1)
[PROOF STATE]
proof (prove)
using this:
rotate_A \<in> simple_rotations
?r \<in> simple_rotations \<Longrightarrow> ?r \<in> complex_rotations

goal (1 subgoal):
 1. rotate_A \<in> complex_rotations
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rotate_A \<in> complex_rotations

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rotate_A \<in> complex_rotations
[PROOF STEP]
have "rotate_A \<in> carrier tetrahedral_group"
[PROOF STATE]
proof (prove)
using this:
rotate_A \<in> complex_rotations

goal (1 subgoal):
 1. rotate_A \<in> carrier tetrahedral_group
[PROOF STEP]
unfolding tetrahedral_group_def partial_object.select_convs(1)
[PROOF STATE]
proof (prove)
using this:
rotate_A \<in> complex_rotations

goal (1 subgoal):
 1. rotate_A \<in> complex_rotations
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rotate_A \<in> carrier tetrahedral_group

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rotate_A \<in> carrier tetrahedral_group

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
have "apply_rotation rotate_A A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_rotation rotate_A A = A
[PROOF STEP]
by (simp add: rotate_A_def)
[PROOF STATE]
proof (state)
this:
apply_rotation rotate_A A = A

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rotate_A \<in> carrier tetrahedral_group
apply_rotation rotate_A A = A
[PROOF STEP]
have A:"rotate_A \<in> (tetrahedral.stabiliser A)"
[PROOF STATE]
proof (prove)
using this:
rotate_A \<in> carrier tetrahedral_group
apply_rotation rotate_A A = A

goal (1 subgoal):
 1. rotate_A \<in> tetrahedral.stabiliser A
[PROOF STEP]
using tetrahedral.stabiliser_def mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
rotate_A \<in> carrier tetrahedral_group
apply_rotation rotate_A A = A
tetrahedral.stabiliser ?x = {g \<in> carrier tetrahedral_group. apply_rotation g ?x = ?x}
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. rotate_A \<in> tetrahedral.stabiliser A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rotate_A \<in> tetrahedral.stabiliser A

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
have "rotate_A \<in> simple_rotations"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotate_A \<in> simple_rotations
[PROOF STEP]
using simple_rotations_def insert_subset subset_insertI
[PROOF STATE]
proof (prove)
using this:
simple_rotations = {id, rotate_A, rotate_B, rotate_C, rotate_D}
(insert ?x ?A \<subseteq> ?B) = (?x \<in> ?B \<and> ?A \<subseteq> ?B)
?B \<subseteq> insert ?a ?B

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

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rotate_A \<in> simple_rotations
[PROOF STEP]
have "rotate_A \<circ> rotate_A \<in> complex_rotations"
[PROOF STATE]
proof (prove)
using this:
rotate_A \<in> simple_rotations

goal (1 subgoal):
 1. rotate_A \<circ> rotate_A \<in> complex_rotations
[PROOF STEP]
using complex_rotations.intros
[PROOF STATE]
proof (prove)
using this:
rotate_A \<in> simple_rotations
?r \<in> simple_rotations \<Longrightarrow> ?r \<in> complex_rotations
\<lbrakk>?r \<in> simple_rotations; ?s \<in> complex_rotations\<rbrakk> \<Longrightarrow> ?r \<circ> ?s \<in> complex_rotations

goal (1 subgoal):
 1. rotate_A \<circ> rotate_A \<in> complex_rotations
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rotate_A \<circ> rotate_A \<in> complex_rotations

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rotate_A \<circ> rotate_A \<in> complex_rotations
[PROOF STEP]
have "rotate_A \<circ> rotate_A \<in> carrier tetrahedral_group"
[PROOF STATE]
proof (prove)
using this:
rotate_A \<circ> rotate_A \<in> complex_rotations

goal (1 subgoal):
 1. rotate_A \<circ> rotate_A \<in> carrier tetrahedral_group
[PROOF STEP]
unfolding tetrahedral_group_def partial_object.select_convs(1)
[PROOF STATE]
proof (prove)
using this:
rotate_A \<circ> rotate_A \<in> complex_rotations

goal (1 subgoal):
 1. rotate_A \<circ> rotate_A \<in> complex_rotations
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rotate_A \<circ> rotate_A \<in> carrier tetrahedral_group

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rotate_A \<circ> rotate_A \<in> carrier tetrahedral_group

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
have "apply_rotation (rotate_A \<circ> rotate_A) A = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_rotation (rotate_A \<circ> rotate_A) A = A
[PROOF STEP]
by (simp add: rotate_A_def)
[PROOF STATE]
proof (state)
this:
apply_rotation (rotate_A \<circ> rotate_A) A = A

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rotate_A \<circ> rotate_A \<in> carrier tetrahedral_group
apply_rotation (rotate_A \<circ> rotate_A) A = A
[PROOF STEP]
have AA:"(rotate_A \<circ> rotate_A) \<in> (tetrahedral.stabiliser A)"
[PROOF STATE]
proof (prove)
using this:
rotate_A \<circ> rotate_A \<in> carrier tetrahedral_group
apply_rotation (rotate_A \<circ> rotate_A) A = A

goal (1 subgoal):
 1. rotate_A \<circ> rotate_A \<in> tetrahedral.stabiliser A
[PROOF STEP]
using tetrahedral.stabiliser_def mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
rotate_A \<circ> rotate_A \<in> carrier tetrahedral_group
apply_rotation (rotate_A \<circ> rotate_A) A = A
tetrahedral.stabiliser ?x = {g \<in> carrier tetrahedral_group. apply_rotation g ?x = ?x}
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. rotate_A \<circ> rotate_A \<in> tetrahedral.stabiliser A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rotate_A \<circ> rotate_A \<in> tetrahedral.stabiliser A

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
from id A AA
[PROOF STATE]
proof (chain)
picking this:
id \<in> tetrahedral.stabiliser A
rotate_A \<in> tetrahedral.stabiliser A
rotate_A \<circ> rotate_A \<in> tetrahedral.stabiliser A
[PROOF STEP]
show "stabiliser_A \<subseteq> tetrahedral.stabiliser A"
[PROOF STATE]
proof (prove)
using this:
id \<in> tetrahedral.stabiliser A
rotate_A \<in> tetrahedral.stabiliser A
rotate_A \<circ> rotate_A \<in> tetrahedral.stabiliser A

goal (1 subgoal):
 1. stabiliser_A \<subseteq> tetrahedral.stabiliser A
[PROOF STEP]
by (simp add: stabiliser_A_def subsetI)
[PROOF STATE]
proof (state)
this:
stabiliser_A \<subseteq> tetrahedral.stabiliser A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
stabiliser_A \<subseteq> tetrahedral.stabiliser A

goal (1 subgoal):
 1. tetrahedral.stabiliser A \<subseteq> stabiliser_A
[PROOF STEP]
show "tetrahedral.stabiliser A \<subseteq> stabiliser_A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tetrahedral.stabiliser A \<subseteq> stabiliser_A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
assume a:"x \<in> tetrahedral.stabiliser A"
[PROOF STATE]
proof (state)
this:
x \<in> tetrahedral.stabiliser A

goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
with tetrahedral.stabiliser_def
[PROOF STATE]
proof (chain)
picking this:
tetrahedral.stabiliser ?x = {g \<in> carrier tetrahedral_group. apply_rotation g ?x = ?x}
x \<in> tetrahedral.stabiliser A
[PROOF STEP]
have "apply_rotation x A = A"
[PROOF STATE]
proof (prove)
using this:
tetrahedral.stabiliser ?x = {g \<in> carrier tetrahedral_group. apply_rotation g ?x = ?x}
x \<in> tetrahedral.stabiliser A

goal (1 subgoal):
 1. apply_rotation x A = A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_rotation x A = A

goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
with apply_rotation.simps
[PROOF STATE]
proof (chain)
picking this:
apply_rotation ?r ?v = ?r ?v
apply_rotation x A = A
[PROOF STEP]
have xA:"x A = A"
[PROOF STATE]
proof (prove)
using this:
apply_rotation ?r ?v = ?r ?v
apply_rotation x A = A

goal (1 subgoal):
 1. x A = A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x A = A

goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
x \<in> tetrahedral.stabiliser A
[PROOF STEP]
have "x \<in> carrier tetrahedral_group"
[PROOF STATE]
proof (prove)
using this:
x \<in> tetrahedral.stabiliser A

goal (1 subgoal):
 1. x \<in> carrier tetrahedral_group
[PROOF STEP]
using subgroup.mem_carrier[of "tetrahedral.stabiliser A"] tetrahedral.stabiliser_subgroup
[PROOF STATE]
proof (prove)
using this:
x \<in> tetrahedral.stabiliser A
\<lbrakk>subgroup (tetrahedral.stabiliser A) ?G; ?x \<in> tetrahedral.stabiliser A\<rbrakk> \<Longrightarrow> ?x \<in> carrier ?G
subgroup (tetrahedral.stabiliser ?x) tetrahedral_group

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

goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> carrier tetrahedral_group
[PROOF STEP]
have xC:"x \<in> complex_rotations"
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier tetrahedral_group

goal (1 subgoal):
 1. x \<in> complex_rotations
[PROOF STEP]
unfolding tetrahedral_group_def partial_object.select_convs(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations

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

goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x B \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x B \<noteq> A
[PROOF STEP]
using xA xC rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x A = A
x \<in> complex_rotations
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x B \<noteq> A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x B \<noteq> A

goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x B \<noteq> A
[PROOF STEP]
have "x \<in> complex_rotations \<Longrightarrow> x A = A \<Longrightarrow> x \<in> stabiliser_A"
[PROOF STATE]
proof (prove)
using this:
x B \<noteq> A

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
proof (cases "x B", simp)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = B\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 3. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
assume "x B = B"
[PROOF STATE]
proof (state)
this:
x B = B

goal (3 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = B\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 3. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x B = B
[PROOF STEP]
have "x = id"
[PROOF STATE]
proof (prove)
using this:
x B = B

goal (1 subgoal):
 1. x = id
[PROOF STEP]
using complex_rotations_fix xC xA
[PROOF STATE]
proof (prove)
using this:
x B = B
\<lbrakk>?r \<in> complex_rotations; ?r ?a = ?a; ?r ?b = ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?r = id
x \<in> complex_rotations
x A = A

goal (1 subgoal):
 1. x = id
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = id

goal (3 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = B\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 3. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = id
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = id

goal (1 subgoal):
 1. x \<in> stabiliser_A
[PROOF STEP]
using stabiliser_A_def
[PROOF STATE]
proof (prove)
using this:
x = id
stabiliser_A = {id, rotate_A, rotate_A \<circ> rotate_A}

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

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
assume "x B = C"
[PROOF STATE]
proof (state)
this:
x B = C

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x B = C
[PROOF STEP]
have "x \<noteq> id"
[PROOF STATE]
proof (prove)
using this:
x B = C

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

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> id
[PROOF STEP]
have "x D \<noteq> D"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> id

goal (1 subgoal):
 1. x D \<noteq> D
[PROOF STEP]
using complex_rotations_fix xC xA
[PROOF STATE]
proof (prove)
using this:
x \<noteq> id
\<lbrakk>?r \<in> complex_rotations; ?r ?a = ?a; ?r ?b = ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?r = id
x \<in> complex_rotations
x A = A

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

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x D \<noteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x D \<noteq> C
[PROOF STEP]
using xC \<open>x B = C\<close> rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations
x B = C
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x D \<noteq> C
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x D \<noteq> C

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x D \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x D \<noteq> A
[PROOF STEP]
using xC xA rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations
x A = A
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x D \<noteq> A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x D \<noteq> A

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x D \<noteq> A
[PROOF STEP]
have "x D = B"
[PROOF STATE]
proof (prove)
using this:
x D \<noteq> A

goal (1 subgoal):
 1. x D = B
[PROOF STEP]
using \<open>x D \<noteq> C\<close>  \<open>x D \<noteq> D\<close> Vertex.exhaust
[PROOF STATE]
proof (prove)
using this:
x D \<noteq> A
x D \<noteq> C
x D \<noteq> D
\<lbrakk>?y = A \<Longrightarrow> ?P; ?y = B \<Longrightarrow> ?P; ?y = C \<Longrightarrow> ?P; ?y = D \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. x D = B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x D = B

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x C \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x C \<noteq> A
[PROOF STEP]
using xC xA rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations
x A = A
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x C \<noteq> A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x C \<noteq> A

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x C \<noteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x C \<noteq> B
[PROOF STEP]
using xC \<open>x D = B\<close> rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations
x D = B
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x C \<noteq> B
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x C \<noteq> B

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x C \<noteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x C \<noteq> C
[PROOF STEP]
using complex_rotations_fix xC xA \<open>x \<noteq> id\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r \<in> complex_rotations; ?r ?a = ?a; ?r ?b = ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?r = id
x \<in> complex_rotations
x A = A
x \<noteq> id

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

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x C \<noteq> C
[PROOF STEP]
have "x C = D"
[PROOF STATE]
proof (prove)
using this:
x C \<noteq> C

goal (1 subgoal):
 1. x C = D
[PROOF STEP]
using \<open>x C \<noteq> A\<close> \<open>x C \<noteq> B\<close> Vertex.exhaust
[PROOF STATE]
proof (prove)
using this:
x C \<noteq> C
x C \<noteq> A
x C \<noteq> B
\<lbrakk>?y = A \<Longrightarrow> ?P; ?y = B \<Longrightarrow> ?P; ?y = C \<Longrightarrow> ?P; ?y = D \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. x C = D
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x C = D

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "\<forall> v. x v = rotate_A v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v. x v = rotate_A v
[PROOF STEP]
using xA \<open>x B = C\<close> \<open>x D = B\<close> \<open>x C = D\<close> Vertex.exhaust rotate_A_def Vertex.simps
[PROOF STATE]
proof (prove)
using this:
x A = A
x B = C
x D = B
x C = D
\<lbrakk>?y = A \<Longrightarrow> ?P; ?y = B \<Longrightarrow> ?P; ?y = C \<Longrightarrow> ?P; ?y = D \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
rotate_A = (\<lambda>v. case v of A \<Rightarrow> A | B \<Rightarrow> C | C \<Rightarrow> D | D \<Rightarrow> B)
A \<noteq> B
B \<noteq> A
A \<noteq> C
C \<noteq> A
A \<noteq> D
D \<noteq> A
B \<noteq> C
C \<noteq> B
B \<noteq> D
D \<noteq> B
C \<noteq> D
D \<noteq> C
(case A of A \<Rightarrow> ?f1.0 | B \<Rightarrow> ?f2.0 | C \<Rightarrow> ?f3.0 | D \<Rightarrow> ?f4.0) = ?f1.0
(case B of A \<Rightarrow> ?f1.0 | B \<Rightarrow> ?f2.0 | C \<Rightarrow> ?f3.0 | D \<Rightarrow> ?f4.0) = ?f2.0
(case C of A \<Rightarrow> ?f1.0 | B \<Rightarrow> ?f2.0 | C \<Rightarrow> ?f3.0 | D \<Rightarrow> ?f4.0) = ?f3.0
(case D of A \<Rightarrow> ?f1.0 | B \<Rightarrow> ?f2.0 | C \<Rightarrow> ?f3.0 | D \<Rightarrow> ?f4.0) = ?f4.0
rec_Vertex ?f1.0 ?f2.0 ?f3.0 ?f4.0 A = ?f1.0
rec_Vertex ?f1.0 ?f2.0 ?f3.0 ?f4.0 B = ?f2.0
rec_Vertex ?f1.0 ?f2.0 ?f3.0 ?f4.0 C = ?f3.0
rec_Vertex ?f1.0 ?f2.0 ?f3.0 ?f4.0 D = ?f4.0

goal (1 subgoal):
 1. \<forall>v. x v = rotate_A v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>v. x v = rotate_A v

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v. x v = rotate_A v
[PROOF STEP]
have "x = rotate_A"
[PROOF STATE]
proof (prove)
using this:
\<forall>v. x v = rotate_A v

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

goal (2 subgoals):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = C\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
 2. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = rotate_A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = rotate_A

goal (1 subgoal):
 1. x \<in> stabiliser_A
[PROOF STEP]
using stabiliser_A_def
[PROOF STATE]
proof (prove)
using this:
x = rotate_A
stabiliser_A = {id, rotate_A, rotate_A \<circ> rotate_A}

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

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
assume "x B = D"
[PROOF STATE]
proof (state)
this:
x B = D

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x B = D
[PROOF STEP]
have "x \<noteq> id"
[PROOF STATE]
proof (prove)
using this:
x B = D

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

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> id
[PROOF STEP]
have "x C \<noteq> C"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> id

goal (1 subgoal):
 1. x C \<noteq> C
[PROOF STEP]
using complex_rotations_fix xC xA
[PROOF STATE]
proof (prove)
using this:
x \<noteq> id
\<lbrakk>?r \<in> complex_rotations; ?r ?a = ?a; ?r ?b = ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?r = id
x \<in> complex_rotations
x A = A

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

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x C \<noteq> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x C \<noteq> D
[PROOF STEP]
using xC \<open>x B = D\<close> rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations
x B = D
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x C \<noteq> D
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x C \<noteq> D

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x C \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x C \<noteq> A
[PROOF STEP]
using xC xA rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations
x A = A
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x C \<noteq> A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x C \<noteq> A

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x C \<noteq> A
[PROOF STEP]
have "x C = B"
[PROOF STATE]
proof (prove)
using this:
x C \<noteq> A

goal (1 subgoal):
 1. x C = B
[PROOF STEP]
using \<open>x C \<noteq> D\<close>  \<open>x C \<noteq> C\<close> Vertex.exhaust
[PROOF STATE]
proof (prove)
using this:
x C \<noteq> A
x C \<noteq> D
x C \<noteq> C
\<lbrakk>?y = A \<Longrightarrow> ?P; ?y = B \<Longrightarrow> ?P; ?y = C \<Longrightarrow> ?P; ?y = D \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. x C = B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x C = B

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x D \<noteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x D \<noteq> A
[PROOF STEP]
using xC xA rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations
x A = A
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x D \<noteq> A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x D \<noteq> A

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x D \<noteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x D \<noteq> B
[PROOF STEP]
using xC \<open>x C = B\<close> rotation_bij_corollary
[PROOF STATE]
proof (prove)
using this:
x \<in> complex_rotations
x C = B
?r \<in> complex_rotations \<Longrightarrow> (?r ?x \<noteq> ?r ?y) = (?x \<noteq> ?y)

goal (1 subgoal):
 1. x D \<noteq> B
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x D \<noteq> B

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "x D \<noteq> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x D \<noteq> D
[PROOF STEP]
using complex_rotations_fix xC xA \<open>x \<noteq> id\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r \<in> complex_rotations; ?r ?a = ?a; ?r ?b = ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?r = id
x \<in> complex_rotations
x A = A
x \<noteq> id

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

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x D \<noteq> D
[PROOF STEP]
have "x D = C"
[PROOF STATE]
proof (prove)
using this:
x D \<noteq> D

goal (1 subgoal):
 1. x D = C
[PROOF STEP]
using \<open>x D \<noteq> A\<close> \<open>x D \<noteq> B\<close> Vertex.exhaust
[PROOF STATE]
proof (prove)
using this:
x D \<noteq> D
x D \<noteq> A
x D \<noteq> B
\<lbrakk>?y = A \<Longrightarrow> ?P; ?y = B \<Longrightarrow> ?P; ?y = C \<Longrightarrow> ?P; ?y = D \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. x D = C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x D = C

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
have "\<forall> v. x v = (rotate_A \<circ> rotate_A) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v. x v = (rotate_A \<circ> rotate_A) v
[PROOF STEP]
using xA \<open>x B = D\<close> \<open>x C = B\<close> \<open>x D = C\<close> Vertex.exhaust rotate_A_def Vertex.simps comp_apply
[PROOF STATE]
proof (prove)
using this:
x A = A
x B = D
x C = B
x D = C
\<lbrakk>?y = A \<Longrightarrow> ?P; ?y = B \<Longrightarrow> ?P; ?y = C \<Longrightarrow> ?P; ?y = D \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
rotate_A = (\<lambda>v. case v of A \<Rightarrow> A | B \<Rightarrow> C | C \<Rightarrow> D | D \<Rightarrow> B)
A \<noteq> B
B \<noteq> A
A \<noteq> C
C \<noteq> A
A \<noteq> D
D \<noteq> A
B \<noteq> C
C \<noteq> B
B \<noteq> D
D \<noteq> B
C \<noteq> D
D \<noteq> C
(case A of A \<Rightarrow> ?f1.0 | B \<Rightarrow> ?f2.0 | C \<Rightarrow> ?f3.0 | D \<Rightarrow> ?f4.0) = ?f1.0
(case B of A \<Rightarrow> ?f1.0 | B \<Rightarrow> ?f2.0 | C \<Rightarrow> ?f3.0 | D \<Rightarrow> ?f4.0) = ?f2.0
(case C of A \<Rightarrow> ?f1.0 | B \<Rightarrow> ?f2.0 | C \<Rightarrow> ?f3.0 | D \<Rightarrow> ?f4.0) = ?f3.0
(case D of A \<Rightarrow> ?f1.0 | B \<Rightarrow> ?f2.0 | C \<Rightarrow> ?f3.0 | D \<Rightarrow> ?f4.0) = ?f4.0
rec_Vertex ?f1.0 ?f2.0 ?f3.0 ?f4.0 A = ?f1.0
rec_Vertex ?f1.0 ?f2.0 ?f3.0 ?f4.0 B = ?f2.0
rec_Vertex ?f1.0 ?f2.0 ?f3.0 ?f4.0 C = ?f3.0
rec_Vertex ?f1.0 ?f2.0 ?f3.0 ?f4.0 D = ?f4.0
(?f \<circ> ?g) ?x = ?f (?g ?x)

goal (1 subgoal):
 1. \<forall>v. x v = (rotate_A \<circ> rotate_A) v
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>v. x v = (rotate_A \<circ> rotate_A) v

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v. x v = (rotate_A \<circ> rotate_A) v
[PROOF STEP]
have "x = rotate_A \<circ> rotate_A"
[PROOF STATE]
proof (prove)
using this:
\<forall>v. x v = (rotate_A \<circ> rotate_A) v

goal (1 subgoal):
 1. x = rotate_A \<circ> rotate_A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = rotate_A \<circ> rotate_A

goal (1 subgoal):
 1. \<lbrakk>x \<in> complex_rotations; x A = A; x B \<noteq> A; x B = D\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = rotate_A \<circ> rotate_A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = rotate_A \<circ> rotate_A

goal (1 subgoal):
 1. x \<in> stabiliser_A
[PROOF STEP]
using stabiliser_A_def
[PROOF STATE]
proof (prove)
using this:
x = rotate_A \<circ> rotate_A
stabiliser_A = {id, rotate_A, rotate_A \<circ> rotate_A}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<in> complex_rotations; x A = A\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A

goal (1 subgoal):
 1. \<And>x. x \<in> tetrahedral.stabiliser A \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x \<in> complex_rotations; x A = A\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
[PROOF STEP]
show "x \<in> stabiliser_A"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> complex_rotations; x A = A\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A

goal (1 subgoal):
 1. x \<in> stabiliser_A
[PROOF STEP]
using xA xC
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> complex_rotations; x A = A\<rbrakk> \<Longrightarrow> x \<in> stabiliser_A
x A = A
x \<in> complex_rotations

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
tetrahedral.stabiliser A \<subseteq> stabiliser_A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R_abort: "abort \<le> rel_R \<lceil>P\<rceil> \<lceil>Q\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abort \<subseteq> rel_R \<lceil>P\<rceil> \<lceil>Q\<rceil>
[PROOF STEP]
by (rule rel_rkat.R2, simp)

\<comment> \<open> Sequential Composition \<close>


[STATEMENT]
lemma (in group) IDirProds_is_subgroup:
  assumes "\<Union>(S ` I) \<subseteq> (carrier G)"
  shows "subgroup (IDirProds G S I) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (IDirProds G S I) G
[PROOF STEP]
unfolding IDirProds_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (generate G (\<Union> (S ` I))) G
[PROOF STEP]
using generate_is_subgroup[of "\<Union>(S ` I)"] assms
[PROOF STATE]
proof (prove)
using this:
\<Union> (S ` I) \<subseteq> carrier G \<Longrightarrow> subgroup (generate G (\<Union> (S ` I))) G
\<Union> (S ` I) \<subseteq> carrier G

goal (1 subgoal):
 1. subgroup (generate G (\<Union> (S ` I))) G
[PROOF STEP]
by auto


[STATEMENT]
lemma hurwitz_zeta_0 [simp]: "a > 0 \<Longrightarrow> hurwitz_zeta a 0 = 1 / 2 - a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < a \<Longrightarrow> hurwitz_zeta a 0 = complex_of_real (1 / 2 - a)
[PROOF STEP]
using hurwitz_zeta_neg_of_nat[of a 0]
[PROOF STATE]
proof (prove)
using this:
0 < a \<Longrightarrow> hurwitz_zeta a (- of_nat 0) = complex_of_real (- bernpoly (Suc 0) a / real (Suc 0))

goal (1 subgoal):
 1. 0 < a \<Longrightarrow> hurwitz_zeta a 0 = complex_of_real (1 / 2 - a)
[PROOF STEP]
by (simp add: bernpoly_def)


[STATEMENT]
lemma  di (*[simp]*):"d \<inter> d^-1 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<inter> d\<inverse> = {}
[PROOF STEP]
apply (auto simp:d)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b k ka l la u ua v va. \<lbrakk>k \<parallel> l; ka \<parallel> la; l \<parallel> a; la \<parallel> b; a \<parallel> u; b \<parallel> ua; u \<parallel> v; ua \<parallel> va; k \<parallel> b; b \<parallel> v; ka \<parallel> a; a \<parallel> va\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (meson M1 trans2)


[STATEMENT]
lemma  arcs_blocks_ends: "(x, y) \<in> arcs_ends G \<Longrightarrow> {x, y} \<in># arcs_blocks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<rightarrow> y \<Longrightarrow> {x, y} \<in># arcs_blocks
[PROOF STEP]
proof (auto simp add: arcs_ends_def arcs_blocks_def )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, y) = arc_to_ends G xa; xa \<in> arcs G\<rbrakk> \<Longrightarrow> {x, y} \<in> arc_to_block ` arcs G
[PROOF STEP]
fix xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, y) = arc_to_ends G xa; xa \<in> arcs G\<rbrakk> \<Longrightarrow> {x, y} \<in> arc_to_block ` arcs G
[PROOF STEP]
assume assm1: "(x, y) = arc_to_ends G xa" and assm2: "xa \<in> arcs G"
[PROOF STATE]
proof (state)
this:
(x, y) = arc_to_ends G xa
xa \<in> arcs G

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, y) = arc_to_ends G xa; xa \<in> arcs G\<rbrakk> \<Longrightarrow> {x, y} \<in> arc_to_block ` arcs G
[PROOF STEP]
obtain z where zin: "z \<in> (arc_to_block ` (arcs G))" and "z = arc_to_block xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> arc_to_block ` arcs G; z = arc_to_block xa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assm2
[PROOF STATE]
proof (prove)
using this:
xa \<in> arcs G

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> arc_to_block ` arcs G; z = arc_to_block xa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> arc_to_block ` arcs G
z = arc_to_block xa

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, y) = arc_to_ends G xa; xa \<in> arcs G\<rbrakk> \<Longrightarrow> {x, y} \<in> arc_to_block ` arcs G
[PROOF STEP]
thus "{x, y} \<in> arc_to_block ` (arcs G)"
[PROOF STATE]
proof (prove)
using this:
z \<in> arc_to_block ` arcs G
z = arc_to_block xa

goal (1 subgoal):
 1. {x, y} \<in> arc_to_block ` arcs G
[PROOF STEP]
using assm1 arc_to_block_to_ends
[PROOF STATE]
proof (prove)
using this:
z \<in> arc_to_block ` arcs G
z = arc_to_block xa
(x, y) = arc_to_ends G xa
{fst (arc_to_ends G ?e), snd (arc_to_ends G ?e)} = arc_to_block ?e

goal (1 subgoal):
 1. {x, y} \<in> arc_to_block ` arcs G
[PROOF STEP]
by (metis fst_conv snd_conv)
[PROOF STATE]
proof (state)
this:
{x, y} \<in> arc_to_block ` arcs G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma strong_fermat_witness_iff:
  "strong_fermat_witness =
     (\<exists>k m. odd m \<and> n - 1 = 2 ^ k * m \<and> [a ^ m \<noteq> 1] (mod n) \<and>
            (\<forall>i\<in>{0..<k}. [a ^ (2 ^ i * m) \<noteq> n-1] (mod n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.strong_fermat_witness = (\<exists>k m. odd m \<and> n - 1 = 2 ^ k * m \<and> [a ^ m \<noteq> 1] (mod n) \<and> (\<forall>i\<in>{0..<k}. [a ^ (2 ^ i * m) \<noteq> n - 1] (mod n)))
[PROOF STEP]
unfolding strong_fermat_witness_def strong_fermat_liar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (\<forall>k m. odd m \<longrightarrow> n - 1 = 2 ^ k * m \<longrightarrow> [a ^ m = 1] (mod n) \<or> (\<exists>i\<in>{0..<k}. [a ^ (2 ^ i * m) = n - 1] (mod n)))) = (\<exists>k m. odd m \<and> n - 1 = 2 ^ k * m \<and> [a ^ m \<noteq> 1] (mod n) \<and> (\<forall>i\<in>{0..<k}. [a ^ (2 ^ i * m) \<noteq> n - 1] (mod n)))
[PROOF STEP]
by blast


[STATEMENT]
lemma qbs_prob_integral_morphism':
  assumes "f \<in> X \<rightarrow>\<^sub>Q \<real>\<^sub>Q"
  shows "(\<lambda>s. qbs_prob_integral s f) \<in> monadP_qbs X \<rightarrow>\<^sub>Q \<real>\<^sub>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. qbs_prob_integral s f) \<in> monadP_qbs X \<rightarrow>\<^sub>Q \<real>\<^sub>Q
[PROOF STEP]
proof(rule qbs_morphismI;simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
fix \<alpha>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
assume "\<alpha> \<in> monadP_qbs_MPx X"
[PROOF STATE]
proof (state)
this:
\<alpha> \<in> monadP_qbs_MPx X

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in> monadP_qbs_MPx X
[PROOF STEP]
obtain \<beta> g where h:
   "\<beta> \<in> qbs_Mx X" "g \<in> real_borel \<rightarrow>\<^sub>M prob_algebra real_borel"
   "\<alpha> = (\<lambda>r. qbs_prob_space (X, \<beta>, g r))"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> monadP_qbs_MPx X

goal (1 subgoal):
 1. (\<And>\<beta> g. \<lbrakk>\<beta> \<in> qbs_Mx X; g \<in> real_borel \<rightarrow>\<^sub>M prob_algebra real_borel; \<alpha> = (\<lambda>r. qbs_prob_space (X, \<beta>, g r))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rep_monadP_qbs_MPx[of \<alpha> X]
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> monadP_qbs_MPx X
\<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> \<exists>\<alpha>' g. \<alpha>' \<in> qbs_Mx X \<and> g \<in> real_borel \<rightarrow>\<^sub>M prob_algebra real_borel \<and> \<alpha> = (\<lambda>r. qbs_prob_space (X, \<alpha>', g r))

goal (1 subgoal):
 1. (\<And>\<beta> g. \<lbrakk>\<beta> \<in> qbs_Mx X; g \<in> real_borel \<rightarrow>\<^sub>M prob_algebra real_borel; \<alpha> = (\<lambda>r. qbs_prob_space (X, \<beta>, g r))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<beta> \<in> qbs_Mx X
g \<in> real_borel \<rightarrow>\<^sub>M prob_algebra real_borel
\<alpha> = (\<lambda>r. qbs_prob_space (X, \<beta>, g r))

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
note [measurable] = h(2)
[PROOF STATE]
proof (state)
this:
g \<in> real_borel \<rightarrow>\<^sub>M prob_algebra real_borel

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
have [measurable]: "f \<circ> \<beta> \<in> real_borel \<rightarrow>\<^sub>M real_borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ> \<beta> \<in> borel_measurable real_borel
[PROOF STEP]
using assms h(1)
[PROOF STATE]
proof (prove)
using this:
f \<in> X \<rightarrow>\<^sub>Q \<real>\<^sub>Q
\<beta> \<in> qbs_Mx X

goal (1 subgoal):
 1. f \<circ> \<beta> \<in> borel_measurable real_borel
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<circ> \<beta> \<in> borel_measurable real_borel

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
have "(\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> = (\<lambda>r. \<integral> x. f (\<beta> x) \<partial>g r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> = (\<lambda>r. LINT x|g r. f (\<beta> x))
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. ((\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha>) r = LINT x|g r. f (\<beta> x)
[PROOF STEP]
using assms qbs_prob_MPx[OF h(1,2)]
[PROOF STATE]
proof (prove)
using this:
f \<in> X \<rightarrow>\<^sub>Q \<real>\<^sub>Q
qbs_prob X \<beta> (g ?r)

goal (1 subgoal):
 1. \<And>r. ((\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha>) r = LINT x|g r. f (\<beta> x)
[PROOF STEP]
by(auto intro!: qbs_prob.qbs_prob_integral_def simp: h(3))
[PROOF STATE]
proof (state)
this:
(\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> = (\<lambda>r. LINT x|g r. f (\<beta> x))

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> = (\<lambda>r. LINT x|g r. f (\<beta> x))

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
have "... = (\<lambda>M. integral\<^sup>L M (f \<circ> \<beta>)) \<circ> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>r. LINT x|g r. f (\<beta> x)) = (\<lambda>M. integral\<^sup>L M (f \<circ> \<beta>)) \<circ> g
[PROOF STEP]
by (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>r. LINT x|g r. f (\<beta> x)) = (\<lambda>M. integral\<^sup>L M (f \<circ> \<beta>)) \<circ> g

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>r. LINT x|g r. f (\<beta> x)) = (\<lambda>M. integral\<^sup>L M (f \<circ> \<beta>)) \<circ> g

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
have "... \<in> real_borel \<rightarrow>\<^sub>M real_borel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>M. integral\<^sup>L M (f \<circ> \<beta>)) \<circ> g \<in> borel_measurable real_borel
[PROOF STEP]
by(auto intro!: measurable_comp[where N="subprob_algebra real_borel"]
              simp: integral_measurable_subprob_algebra measurable_prob_algebraD)
[PROOF STATE]
proof (state)
this:
(\<lambda>M. integral\<^sup>L M (f \<circ> \<beta>)) \<circ> g \<in> borel_measurable real_borel

goal (1 subgoal):
 1. \<And>\<alpha>. \<alpha> \<in> monadP_qbs_MPx X \<Longrightarrow> (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
show "(\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> real_borel \<rightarrow>\<^sub>M real_borel"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel

goal (1 subgoal):
 1. (\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>s. qbs_prob_integral s f) \<circ> \<alpha> \<in> borel_measurable real_borel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma register_pair_apply':
  assumes \<open>compatible F G\<close>
  shows \<open>(F; G) (a \<otimes>\<^sub>u b) = (G b) *\<^sub>u (F a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F;G) (a \<otimes>\<^sub>u b) = G b *\<^sub>u F a
[PROOF STEP]
apply (subst register_pair_apply)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. compatible F G
 2. F a *\<^sub>u G b = G b *\<^sub>u F a
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
compatible F G

goal (2 subgoals):
 1. compatible F G
 2. F a *\<^sub>u G b = G b *\<^sub>u F a
[PROOF STEP]
by (auto simp: compatible_def intro: register_preregister)


[STATEMENT]
lemma fv_extRet2J [simp]: "fv (extRet2J e va) \<subseteq> fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (extRet2J e va) \<subseteq> fv e
[PROOF STEP]
by(cases va) simp_all