[STATEMENT]
lemma root_int_floor_pos_pos: assumes x: "x \<ge> 0"
  shows "root_int_floor_pos p x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> root_int_floor_pos p x
[PROOF STEP]
using root_int_main(1)[OF x, of p]
[PROOF STATE]
proof (prove)
using this:
root_int_main p x = (?y, ?b) \<Longrightarrow> 0 \<le> ?y

goal (1 subgoal):
 1. 0 \<le> root_int_floor_pos p x
[PROOF STEP]
unfolding root_int_floor_pos_def
[PROOF STATE]
proof (prove)
using this:
root_int_main p x = (?y, ?b) \<Longrightarrow> 0 \<le> ?y

goal (1 subgoal):
 1. 0 \<le> (if p = 0 then 0 else fst (root_int_main p x))
[PROOF STEP]
by (cases "root_int_main p x", auto)


[STATEMENT]
lemma has_0: "has 0 S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has 0 S
[PROOF STEP]
by (simp add: has_def)


[STATEMENT]
lemma has_extend_witness':
  "\<lbrakk> has n S; hasw xs S; length xs < n \<rbrakk> \<Longrightarrow> \<exists>x. hasw (x # xs) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has n S; hasw xs S; length xs < n\<rbrakk> \<Longrightarrow> \<exists>x. hasw (x # xs) S
[PROOF STEP]
by (simp, blast dest: has_extend_witness)


[STATEMENT]
theorem wls_vsubst_ident[simp]:
assumes "wls s X"
shows "(X #[z // z]_zs) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X #[z // z]_zs = X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wls s X

goal (1 subgoal):
 1. X #[z // z]_zs = X
[PROOF STEP]
by(simp add: vsubst_ident)


[STATEMENT]
lemma finite_funas_term[simp,intro]: "finite (funas_term t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (funas_term t)
[PROOF STEP]
by (induct t, auto)


[STATEMENT]
lemma VxVxV_arr_eq_VVV_arr:
    shows "VxVxV.arr f \<longleftrightarrow> VVV.arr f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VxVxV.arr f = VVV.arr f
[PROOF STEP]
using VVV.arr_char\<^sub>S\<^sub>b\<^sub>C VV.arr_char\<^sub>S\<^sub>b\<^sub>C src_def trg_def inclusion arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
VVV.arr ?f = (arr (fst ?f) \<and> VV.arr (snd ?f) \<and> src (fst ?f) = trg (fst (snd ?f)))
VV.arr ?f = (arr (fst ?f) \<and> arr (snd ?f) \<and> src (fst ?f) = trg (snd ?f))
src ?\<mu> = (if arr ?\<mu> then src\<^sub>B ?\<mu> else null)
trg ?\<mu> = (if arr ?\<mu> then trg\<^sub>B ?\<mu> else null)
B.arr ?f \<and> src\<^sub>B ?f = a \<and> trg\<^sub>B ?f = a \<Longrightarrow> B.arr ?f
arr ?f = (B.arr ?f \<and> src\<^sub>B ?f = a \<and> trg\<^sub>B ?f = a)

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


[STATEMENT]
lemma uniform_limit_at_within_subset:
  assumes "uniform_limit S x l (at t within T)"
  assumes "U \<subseteq> T"
  shows "uniform_limit S x l (at t within U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uniform_limit S x l (at t within U)
[PROOF STEP]
by (metis assms(1) assms(2) eventually_within_Un filterlim_iff subset_Un_eq)


[STATEMENT]
lemma pnet_reachable_transfer':
  assumes "wf_net_tree n"
      and "s \<in> reachable (closed (pnet np n)) TT"
    shows "netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U"
          (is " _ \<in> ?f ` ?oreachable n")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
s \<in> reachable (closed (pnet np n)) TT

goal (1 subgoal):
 1. netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. s \<in> init (closed (pnet np n)) \<Longrightarrow> netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
 2. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. s \<in> init (closed (pnet np n)) \<Longrightarrow> netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
 2. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
assume "s \<in> init (closed (pnet np n))"
[PROOF STATE]
proof (state)
this:
s \<in> init (closed (pnet np n))

goal (2 subgoals):
 1. \<And>s. s \<in> init (closed (pnet np n)) \<Longrightarrow> netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
 2. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
hence "s \<in> init (pnet np n)"
[PROOF STATE]
proof (prove)
using this:
s \<in> init (closed (pnet np n))

goal (1 subgoal):
 1. s \<in> init (pnet np n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<in> init (pnet np n)

goal (2 subgoals):
 1. \<And>s. s \<in> init (closed (pnet np n)) \<Longrightarrow> netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
 2. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
with \<open>wf_net_tree n\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_net_tree n
s \<in> init (pnet np n)
[PROOF STEP]
have "netgmap sr s \<in> netmask (net_tree_ips n) ` init (opnet onp n)"
[PROOF STATE]
proof (prove)
using this:
wf_net_tree n
s \<in> init (pnet np n)

goal (1 subgoal):
 1. netgmap sr s \<in> netmask (net_tree_ips n) ` init (opnet onp n)
[PROOF STEP]
by (rule init_pnet_opnet)
[PROOF STATE]
proof (state)
this:
netgmap sr s \<in> netmask (net_tree_ips n) ` init (opnet onp n)

goal (2 subgoals):
 1. \<And>s. s \<in> init (closed (pnet np n)) \<Longrightarrow> netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
 2. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
hence "netgmap sr s \<in> netmask (net_tree_ips n) ` init (oclosed (opnet onp n))"
[PROOF STATE]
proof (prove)
using this:
netgmap sr s \<in> netmask (net_tree_ips n) ` init (opnet onp n)

goal (1 subgoal):
 1. netgmap sr s \<in> netmask (net_tree_ips n) ` init (oclosed (opnet onp n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
netgmap sr s \<in> netmask (net_tree_ips n) ` init (oclosed (opnet onp n))

goal (2 subgoals):
 1. \<And>s. s \<in> init (closed (pnet np n)) \<Longrightarrow> netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
 2. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
netgmap sr s \<in> netmask (net_tree_ips n) ` init (oclosed (opnet onp n))

goal (2 subgoals):
 1. \<And>s. s \<in> init (closed (pnet np n)) \<Longrightarrow> netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
 2. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
have "netmask (net_tree_ips n) ` init (oclosed (opnet onp n))
                                        \<subseteq> netmask (net_tree_ips n) ` ?oreachable n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. netmask (net_tree_ips n) ` init (oclosed (opnet onp n)) \<subseteq> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
by (intro image_mono subsetI) (rule oreachable_init)
[PROOF STATE]
proof (state)
this:
netmask (net_tree_ips n) ` init (oclosed (opnet onp n)) \<subseteq> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U

goal (2 subgoals):
 1. \<And>s. s \<in> init (closed (pnet np n)) \<Longrightarrow> netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
 2. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
netgmap sr s \<in> netmask (net_tree_ips n) ` init (oclosed (opnet onp n))
netmask (net_tree_ips n) ` init (oclosed (opnet onp n)) \<subseteq> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
show "netgmap sr s \<in> netmask (net_tree_ips n) ` ?oreachable n"
[PROOF STATE]
proof (prove)
using this:
netgmap sr s \<in> netmask (net_tree_ips n) ` init (oclosed (opnet onp n))
netmask (net_tree_ips n) ` init (oclosed (opnet onp n)) \<subseteq> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U

goal (1 subgoal):
 1. netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
by (rule rev_subsetD)
[PROOF STATE]
proof (state)
this:
netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U

goal (1 subgoal):
 1. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
fix s a s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
assume "s \<in> reachable (closed (pnet np n)) TT"
       and "netgmap sr s \<in> netmask (net_tree_ips n) ` ?oreachable n"
       and "(s, a, s') \<in> trans (closed (pnet np n))"
[PROOF STATE]
proof (state)
this:
s \<in> reachable (closed (pnet np n)) TT
netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
(s, a, s') \<in> automaton.trans (closed (pnet np n))

goal (1 subgoal):
 1. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
obtain \<sigma> \<zeta> where "netgmap sr s = netmask (net_tree_ips n) (\<sigma>, \<zeta>)"
                              and "(\<sigma>, \<zeta>) \<in> ?oreachable n"
[PROOF STATE]
proof (prove)
using this:
netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U

goal (1 subgoal):
 1. (\<And>\<sigma> \<zeta>. \<lbrakk>netgmap sr s = netmask (net_tree_ips n) (\<sigma>, \<zeta>); (\<sigma>, \<zeta>) \<in> oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
netgmap sr s = netmask (net_tree_ips n) (\<sigma>, \<zeta>)
(\<sigma>, \<zeta>) \<in> oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U

goal (1 subgoal):
 1. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
from \<open>s \<in> reachable (closed (pnet np n)) TT\<close> this(1) \<open>wf_net_tree n\<close>
         and \<open>(s, a, s') \<in> trans (closed (pnet np n))\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> reachable (closed (pnet np n)) TT
netgmap sr s = netmask (net_tree_ips n) (\<sigma>, \<zeta>)
wf_net_tree n
(s, a, s') \<in> automaton.trans (closed (pnet np n))
[PROOF STEP]
obtain \<sigma>' \<zeta>' where "((\<sigma>, \<zeta>), a, (\<sigma>', \<zeta>')) \<in> trans (oclosed (opnet onp n))"
                     and "netgmap sr s' = netmask (net_tree_ips n) (\<sigma>', \<zeta>')"
[PROOF STATE]
proof (prove)
using this:
s \<in> reachable (closed (pnet np n)) TT
netgmap sr s = netmask (net_tree_ips n) (\<sigma>, \<zeta>)
wf_net_tree n
(s, a, s') \<in> automaton.trans (closed (pnet np n))

goal (1 subgoal):
 1. (\<And>\<sigma>' \<zeta>'. \<lbrakk>((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (oclosed (opnet onp n)); netgmap sr s' = netmask (net_tree_ips n) (\<sigma>', \<zeta>')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule transfer_action)
[PROOF STATE]
proof (state)
this:
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (oclosed (opnet onp n))
netgmap sr s' = netmask (net_tree_ips n) (\<sigma>', \<zeta>')

goal (1 subgoal):
 1. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
from \<open>(\<sigma>, \<zeta>) \<in> ?oreachable n\<close> and this(1)
[PROOF STATE]
proof (chain)
picking this:
(\<sigma>, \<zeta>) \<in> oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (oclosed (opnet onp n))
[PROOF STEP]
have "(\<sigma>', \<zeta>') \<in> ?oreachable n"
[PROOF STATE]
proof (prove)
using this:
(\<sigma>, \<zeta>) \<in> oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
((\<sigma>, \<zeta>), a, \<sigma>', \<zeta>') \<in> automaton.trans (oclosed (opnet onp n))

goal (1 subgoal):
 1. (\<sigma>', \<zeta>') \<in> oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
by (rule oreachable_local) simp
[PROOF STATE]
proof (state)
this:
(\<sigma>', \<zeta>') \<in> oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U

goal (1 subgoal):
 1. \<And>s a s'. \<lbrakk>s \<in> reachable (closed (pnet np n)) TT; netgmap sr s \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U; (s, a, s') \<in> automaton.trans (closed (pnet np n)); TT a\<rbrakk> \<Longrightarrow> netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
with \<open>netgmap sr s' = netmask (net_tree_ips n) (\<sigma>', \<zeta>')\<close>
[PROOF STATE]
proof (chain)
picking this:
netgmap sr s' = netmask (net_tree_ips n) (\<sigma>', \<zeta>')
(\<sigma>', \<zeta>') \<in> oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
show "netgmap sr s' \<in> netmask (net_tree_ips n) ` ?oreachable n"
[PROOF STATE]
proof (prove)
using this:
netgmap sr s' = netmask (net_tree_ips n) (\<sigma>', \<zeta>')
(\<sigma>', \<zeta>') \<in> oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U

goal (1 subgoal):
 1. netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U
[PROOF STEP]
by (rule image_eqI)
[PROOF STATE]
proof (state)
this:
netgmap sr s' \<in> netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (\<lambda>_ _ _. True) U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fbox_test[simp]: "(\<lambda>s. ( |\<questiondown>P?] Q) s) = (\<lambda>s. P s \<longrightarrow> Q s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |\<questiondown>P?] Q = (\<lambda>s. P s \<longrightarrow> Q s)
[PROOF STEP]
unfolding fbox_def test_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>s'. s' \<in> {x. x = s \<and> P x} \<longrightarrow> Q s') = (\<lambda>s. P s \<longrightarrow> Q s)
[PROOF STEP]
by simp

\<comment> \<open> Assignments \<close>


[STATEMENT]
lemma sum_rsub_commutative: "(\<Sum>t=0..(q::nat). \<Sum>R- p l (\<lambda>k. f k t)) = (\<Sum>R- p l (\<lambda>k. \<Sum>t=0..q. f k t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>t = 0..q. \<Sum>R- p l (\<lambda>k. f k t) ) = \<Sum>R- p l (\<lambda>k. sum (f k) {0..q})
[PROOF STEP]
by (rule sum_commutative sum_rsub.simps) +


[STATEMENT]
lemma hfunI [intro]:
  assumes "F \<le> A * B"
  and "\<And>X. X \<^bold>\<in> A \<Longrightarrow> \<exists>!Y. \<langle>X, Y\<rangle> \<^bold>\<in> F"
  and "\<And>X Y. \<langle>X, Y\<rangle> \<^bold>\<in> F \<Longrightarrow> Y \<^bold>\<in> B"
  shows "hfun A B F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hfun A B F
[PROOF STEP]
unfolding hfun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<le> A * B \<and> hfunction F \<and> hdomain F = A \<and> hrange F \<le> B
[PROOF STEP]
using assms hfunction_def hrelation_def is_hpair_def hrange_def hconverse_def hdomain_def
[PROOF STATE]
proof (prove)
using this:
F \<le> A * B
?X \<^bold>\<in> A \<Longrightarrow> \<exists>!Y. \<langle>?X, Y\<rangle> \<^bold>\<in> F
\<langle>?X, ?Y\<rangle> \<^bold>\<in> F \<Longrightarrow> ?Y \<^bold>\<in> B
hfunction ?r = (\<forall>x y. \<langle>x, y\<rangle> \<^bold>\<in> ?r \<longrightarrow> (\<forall>y'. \<langle>x, y'\<rangle> \<^bold>\<in> ?r \<longrightarrow> y = y'))
hrelation ?r = (\<forall>z. z \<^bold>\<in> ?r \<longrightarrow> is_hpair z)
is_hpair ?z = (\<exists>x y. ?z = \<langle>x, y\<rangle>)
hrange ?r = hdomain (hconverse ?r)
hconverse ?r = \<lbrace>z . w \<^bold>\<in> ?r, \<exists>x y. w = \<langle>x, y\<rangle> \<and> z = \<langle>y, x\<rangle>\<rbrace>
hdomain ?r = \<lbrace>x . w \<^bold>\<in> ?r, \<exists>y. w = \<langle>x, y\<rangle>\<rbrace>

goal (1 subgoal):
 1. F \<le> A * B \<and> hfunction F \<and> hdomain F = A \<and> hrange F \<le> B
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>F \<le> A * B; \<And>X. X \<^bold>\<in> A \<Longrightarrow> \<exists>!Y. \<langle>X, Y\<rangle> \<^bold>\<in> F; \<And>X Y. \<langle>X, Y\<rangle> \<^bold>\<in> F \<Longrightarrow> Y \<^bold>\<in> B; \<And>r. hfunction r = (\<forall>x y. \<langle>x, y\<rangle> \<^bold>\<in> r \<longrightarrow> (\<forall>y'. \<langle>x, y'\<rangle> \<^bold>\<in> r \<longrightarrow> y = y')); \<And>r. hrelation r = (\<forall>z. z \<^bold>\<in> r \<longrightarrow> is_hpair z); \<And>z. is_hpair z = (\<exists>x y. z = \<langle>x, y\<rangle>); \<And>r. hrange r = hdomain (hconverse r); \<And>r. hconverse r = \<lbrace>z . w \<^bold>\<in> r, \<exists>x y. w = \<langle>x, y\<rangle> \<and> z = \<langle>y, x\<rangle>\<rbrace>; \<And>r. hdomain r = \<lbrace>x . w \<^bold>\<in> r, \<exists>y. w = \<langle>x, y\<rangle>\<rbrace>\<rbrakk> \<Longrightarrow> F \<le> A * B
 2. \<lbrakk>F \<le> A * B; \<And>X. X \<^bold>\<in> A \<Longrightarrow> \<exists>!Y. \<langle>X, Y\<rangle> \<^bold>\<in> F; \<And>X Y. \<langle>X, Y\<rangle> \<^bold>\<in> F \<Longrightarrow> Y \<^bold>\<in> B; \<And>r. hfunction r = (\<forall>x y. \<langle>x, y\<rangle> \<^bold>\<in> r \<longrightarrow> (\<forall>y'. \<langle>x, y'\<rangle> \<^bold>\<in> r \<longrightarrow> y = y')); \<And>r. hrelation r = (\<forall>z. z \<^bold>\<in> r \<longrightarrow> is_hpair z); \<And>z. is_hpair z = (\<exists>x y. z = \<langle>x, y\<rangle>); \<And>r. hrange r = hdomain (hconverse r); \<And>r. hconverse r = \<lbrace>z . w \<^bold>\<in> r, \<exists>x y. w = \<langle>x, y\<rangle> \<and> z = \<langle>y, x\<rangle>\<rbrace>; \<And>r. hdomain r = \<lbrace>x . w \<^bold>\<in> r, \<exists>y. w = \<langle>x, y\<rangle>\<rbrace>\<rbrakk> \<Longrightarrow> hfunction F
 3. \<lbrakk>F \<le> A * B; \<And>X. X \<^bold>\<in> A \<Longrightarrow> \<exists>!Y. \<langle>X, Y\<rangle> \<^bold>\<in> F; \<And>X Y. \<langle>X, Y\<rangle> \<^bold>\<in> F \<Longrightarrow> Y \<^bold>\<in> B; \<And>r. hfunction r = (\<forall>x y. \<langle>x, y\<rangle> \<^bold>\<in> r \<longrightarrow> (\<forall>y'. \<langle>x, y'\<rangle> \<^bold>\<in> r \<longrightarrow> y = y')); \<And>r. hrelation r = (\<forall>z. z \<^bold>\<in> r \<longrightarrow> is_hpair z); \<And>z. is_hpair z = (\<exists>x y. z = \<langle>x, y\<rangle>); \<And>r. hrange r = hdomain (hconverse r); \<And>r. hconverse r = \<lbrace>z . w \<^bold>\<in> r, \<exists>x y. w = \<langle>x, y\<rangle> \<and> z = \<langle>y, x\<rangle>\<rbrace>; \<And>r. hdomain r = \<lbrace>x . w \<^bold>\<in> r, \<exists>y. w = \<langle>x, y\<rangle>\<rbrace>\<rbrakk> \<Longrightarrow> hdomain F = A
 4. \<lbrakk>F \<le> A * B; \<And>X. X \<^bold>\<in> A \<Longrightarrow> \<exists>!Y. \<langle>X, Y\<rangle> \<^bold>\<in> F; \<And>X Y. \<langle>X, Y\<rangle> \<^bold>\<in> F \<Longrightarrow> Y \<^bold>\<in> B; \<And>r. hfunction r = (\<forall>x y. \<langle>x, y\<rangle> \<^bold>\<in> r \<longrightarrow> (\<forall>y'. \<langle>x, y'\<rangle> \<^bold>\<in> r \<longrightarrow> y = y')); \<And>r. hrelation r = (\<forall>z. z \<^bold>\<in> r \<longrightarrow> is_hpair z); \<And>z. is_hpair z = (\<exists>x y. z = \<langle>x, y\<rangle>); \<And>r. hrange r = hdomain (hconverse r); \<And>r. hconverse r = \<lbrace>z . w \<^bold>\<in> r, \<exists>x y. w = \<langle>x, y\<rangle> \<and> z = \<langle>y, x\<rangle>\<rbrace>; \<And>r. hdomain r = \<lbrace>x . w \<^bold>\<in> r, \<exists>y. w = \<langle>x, y\<rangle>\<rbrace>\<rbrakk> \<Longrightarrow> hrange F \<le> B
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<le> A * B; \<And>X. X \<^bold>\<in> A \<Longrightarrow> \<exists>!Y. \<langle>X, Y\<rangle> \<^bold>\<in> F; \<And>X Y. \<langle>X, Y\<rangle> \<^bold>\<in> F \<Longrightarrow> Y \<^bold>\<in> B; \<And>r. hfunction r = (\<forall>x y. \<langle>x, y\<rangle> \<^bold>\<in> r \<longrightarrow> (\<forall>y'. \<langle>x, y'\<rangle> \<^bold>\<in> r \<longrightarrow> y = y')); \<And>r. hrelation r = (\<forall>z. z \<^bold>\<in> r \<longrightarrow> (\<exists>x y. z = \<langle>x, y\<rangle>)); \<And>z. is_hpair z = (\<exists>x y. z = \<langle>x, y\<rangle>); \<And>r. hrange r = \<lbrace>x . w \<^bold>\<in> \<lbrace>z . w \<^bold>\<in> r, \<exists>x y. w = \<langle>x, y\<rangle> \<and> z = \<langle>y, x\<rangle>\<rbrace>, \<exists>y. w = \<langle>x, y\<rangle>\<rbrace>; \<And>r. hconverse r = \<lbrace>z . w \<^bold>\<in> r, \<exists>x y. w = \<langle>x, y\<rangle> \<and> z = \<langle>y, x\<rangle>\<rbrace>; \<And>r. hdomain r = \<lbrace>x . w \<^bold>\<in> r, \<exists>y. w = \<langle>x, y\<rangle>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>x . w \<^bold>\<in> F, \<exists>y. w = \<langle>x, y\<rangle>\<rbrace> = A
[PROOF STEP]
by fast


[STATEMENT]
lemma hfun_to_arr_hcomp:
    assumes "hfun A B F" and "hfun B C G"
    shows "hfun_to_arr A C (hcomp G F) = comp (hfun_to_arr B C G) (hfun_to_arr A B F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
have 1: "arr_to_hfun (hfun_to_arr A C (hcomp G F)) =
               arr_to_hfun (comp (hfun_to_arr B C G) (hfun_to_arr A B F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
[PROOF STEP]
have "arr_to_hfun (comp (hfun_to_arr B C G) (hfun_to_arr A B F)) =
              hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)) = hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F))
[PROOF STEP]
using assms arr_to_hfun_comp hfun_to_arr_in_hom
[PROOF STATE]
proof (prove)
using this:
hfun A B F
hfun B C G
seq ?g ?f \<Longrightarrow> arr_to_hfun (local.comp ?g ?f) = hcomp (arr_to_hfun ?g) (arr_to_hfun ?f)
hfun ?B ?C ?F \<Longrightarrow> \<guillemotleft>hfun_to_arr ?B ?C ?F : hf_to_ide ?B \<rightarrow> hf_to_ide ?C\<guillemotright>

goal (1 subgoal):
 1. arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)) = hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)) = hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F))

goal (1 subgoal):
 1. arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)) = hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F))

goal (1 subgoal):
 1. arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
[PROOF STEP]
have "... = hcomp G F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F)) = hcomp G F
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hfun A B F
hfun B C G

goal (1 subgoal):
 1. hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F)) = hcomp G F
[PROOF STEP]
by (simp add: arr_to_hfun_hfun_to_arr)
[PROOF STATE]
proof (state)
this:
hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F)) = hcomp G F

goal (1 subgoal):
 1. arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hcomp (arr_to_hfun (hfun_to_arr B C G)) (arr_to_hfun (hfun_to_arr A B F)) = hcomp G F

goal (1 subgoal):
 1. arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
[PROOF STEP]
have "... = arr_to_hfun (hfun_to_arr A C (hcomp G F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hcomp G F = arr_to_hfun (hfun_to_arr A C (hcomp G F))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hcomp G F = arr_to_hfun (hfun_to_arr A C (hcomp G F))
[PROOF STEP]
have "hfun A C (hcomp G F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hfun A C (hcomp G F)
[PROOF STEP]
using assms hfun_hcomp
[PROOF STATE]
proof (prove)
using this:
hfun A B F
hfun B C G
\<lbrakk>hfun ?A ?B ?F; hfun ?B ?C ?G\<rbrakk> \<Longrightarrow> hfun ?A ?C (hcomp ?G ?F)

goal (1 subgoal):
 1. hfun A C (hcomp G F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hfun A C (hcomp G F)

goal (1 subgoal):
 1. hcomp G F = arr_to_hfun (hfun_to_arr A C (hcomp G F))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
hfun A C (hcomp G F)

goal (1 subgoal):
 1. hcomp G F = arr_to_hfun (hfun_to_arr A C (hcomp G F))
[PROOF STEP]
by (simp add: arr_to_hfun_hfun_to_arr)
[PROOF STATE]
proof (state)
this:
hcomp G F = arr_to_hfun (hfun_to_arr A C (hcomp G F))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hcomp G F = arr_to_hfun (hfun_to_arr A C (hcomp G F))

goal (1 subgoal):
 1. arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)) = arr_to_hfun (hfun_to_arr A C (hcomp G F))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)) = arr_to_hfun (hfun_to_arr A C (hcomp G F))

goal (1 subgoal):
 1. arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
have "hfun_to_arr A C (hcomp G F) \<in> hom (hf_to_ide A) (hf_to_ide C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) \<in> hom (hf_to_ide A) (hf_to_ide C)
[PROOF STEP]
using assms hfun_hcomp hf_to_ide_def hfun_to_arr_in_hom
[PROOF STATE]
proof (prove)
using this:
hfun A B F
hfun B C G
\<lbrakk>hfun ?A ?B ?F; hfun ?B ?C ?G\<rbrakk> \<Longrightarrow> hfun ?A ?C (hcomp ?G ?F)
hf_to_ide ?x = mkIde (arr_of ` hfset ?x)
hfun ?B ?C ?F \<Longrightarrow> \<guillemotleft>hfun_to_arr ?B ?C ?F : hf_to_ide ?B \<rightarrow> hf_to_ide ?C\<guillemotright>

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) \<in> hom (hf_to_ide A) (hf_to_ide C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hfun_to_arr A C (hcomp G F) \<in> hom (hf_to_ide A) (hf_to_ide C)

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hfun_to_arr A C (hcomp G F) \<in> hom (hf_to_ide A) (hf_to_ide C)

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
have "comp (hfun_to_arr B C G) (hfun_to_arr A B F)
                          \<in> hom (hf_to_ide A) (hf_to_ide C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.comp (hfun_to_arr B C G) (hfun_to_arr A B F) \<in> hom (hf_to_ide A) (hf_to_ide C)
[PROOF STEP]
using assms hfun_to_arr_in_hom hf_to_ide_def
[PROOF STATE]
proof (prove)
using this:
hfun A B F
hfun B C G
hfun ?B ?C ?F \<Longrightarrow> \<guillemotleft>hfun_to_arr ?B ?C ?F : hf_to_ide ?B \<rightarrow> hf_to_ide ?C\<guillemotright>
hf_to_ide ?x = mkIde (arr_of ` hfset ?x)

goal (1 subgoal):
 1. local.comp (hfun_to_arr B C G) (hfun_to_arr A B F) \<in> hom (hf_to_ide A) (hf_to_ide C)
[PROOF STEP]
by (metis (no_types, lifting) comp_in_homI mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
local.comp (hfun_to_arr B C G) (hfun_to_arr A B F) \<in> hom (hf_to_ide A) (hf_to_ide C)

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.comp (hfun_to_arr B C G) (hfun_to_arr A B F) \<in> hom (hf_to_ide A) (hf_to_ide C)

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
have "inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))
[PROOF STEP]
have "ide (hf_to_ide A) \<and> ide (hf_to_ide C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (hf_to_ide A) \<and> ide (hf_to_ide C)
[PROOF STEP]
using assms hf_to_ide_mapsto
[PROOF STATE]
proof (prove)
using this:
hfun A B F
hfun B C G
hf_to_ide \<in> UNIV \<rightarrow> Collect ide

goal (1 subgoal):
 1. ide (hf_to_ide A) \<and> ide (hf_to_ide C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ide (hf_to_ide A) \<and> ide (hf_to_ide C)

goal (1 subgoal):
 1. inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ide (hf_to_ide A) \<and> ide (hf_to_ide C)

goal (1 subgoal):
 1. inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))
[PROOF STEP]
using bij_betw_hom_hfun [of "hf_to_ide A" "hf_to_ide C"] bij_betw_imp_inj_on
[PROOF STATE]
proof (prove)
using this:
ide (hf_to_ide A) \<and> ide (hf_to_ide C)
\<lbrakk>ide (hf_to_ide A); ide (hf_to_ide C)\<rbrakk> \<Longrightarrow> bij_betw arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C)) {F. hfun (ide_to_hf (hf_to_ide A)) (ide_to_hf (hf_to_ide C)) F}
bij_betw ?f ?A ?B \<Longrightarrow> inj_on ?f ?A

goal (1 subgoal):
 1. inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hfun_to_arr A C (hcomp G F) \<in> hom (hf_to_ide A) (hf_to_ide C)
local.comp (hfun_to_arr B C G) (hfun_to_arr A B F) \<in> hom (hf_to_ide A) (hf_to_ide C)
inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hfun_to_arr A C (hcomp G F) \<in> hom (hf_to_ide A) (hf_to_ide C)
local.comp (hfun_to_arr B C G) (hfun_to_arr A B F) \<in> hom (hf_to_ide A) (hf_to_ide C)
inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
using 1 inj_on_def [of arr_to_hfun "hom (hf_to_ide A) (hf_to_ide C)"]
[PROOF STATE]
proof (prove)
using this:
hfun_to_arr A C (hcomp G F) \<in> hom (hf_to_ide A) (hf_to_ide C)
local.comp (hfun_to_arr B C G) (hfun_to_arr A B F) \<in> hom (hf_to_ide A) (hf_to_ide C)
inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C))
arr_to_hfun (hfun_to_arr A C (hcomp G F)) = arr_to_hfun (local.comp (hfun_to_arr B C G) (hfun_to_arr A B F))
inj_on arr_to_hfun (hom (hf_to_ide A) (hf_to_ide C)) = (\<forall>x\<in>hom (hf_to_ide A) (hf_to_ide C). \<forall>y\<in>hom (hf_to_ide A) (hf_to_ide C). arr_to_hfun x = arr_to_hfun y \<longrightarrow> x = y)

goal (1 subgoal):
 1. hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hfun_to_arr A C (hcomp G F) = local.comp (hfun_to_arr B C G) (hfun_to_arr A B F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma l3_inv5_derived: "l3_inv2 \<inter> l3_inv3 \<subseteq> l3_inv5"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l3_inv2 \<inter> l3_inv3 \<subseteq> l3_inv5
[PROOF STEP]
by (auto simp add: abs_validSet dy_fake_msg_def intro!: l3_inv5I
            dest!: l3_inv3D [THEN synth_mono, THEN [2] rev_subsetD]
            dest!: synth_analz_NI_I_K_synth_analz_NI_E [THEN [2] rev_subsetD])


[STATEMENT]
lemma l3_inv8_derived [iff]:
  "l3_inv2 \<inter> l3_inv3 \<inter> l3_inv4 \<subseteq> l3_inv8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l3_inv2 \<inter> l3_inv3 \<inter> l3_inv4 \<subseteq> l3_inv8
[PROOF STEP]
apply (auto intro!: l3_inv8I dest!: l3_inv3D l3_inv2D)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x A B M. \<lbrakk>x \<in> l3_inv4; Keys_bad (ik x) (l3_state.bad x); analz (ik x) \<subseteq> synth (analz (ik x \<inter> payload \<union> ik x \<inter> valid \<union> ik x \<inter> range LtK \<union> Tags)); implAuth A B M \<in> synth (analz (ik x)); M \<in> payload; implAuth A B M \<notin> ik x\<rbrakk> \<Longrightarrow> M \<in> synth (analz (ik x))
 2. \<And>x A B M. \<lbrakk>x \<in> l3_inv4; Keys_bad (ik x) (l3_state.bad x); analz (ik x) \<subseteq> synth (analz (ik x \<inter> payload \<union> ik x \<inter> valid \<union> ik x \<inter> range LtK \<union> Tags)); implAuth A B M \<in> synth (analz (ik x)); M \<in> payload; implAuth A B M \<notin> ik x; B \<notin> l3_state.bad x\<rbrakk> \<Longrightarrow> A \<in> l3_state.bad x
[PROOF STEP]
text \<open>2 subgoals: M is deducible and the agents are bad\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x A B M. \<lbrakk>x \<in> l3_inv4; Keys_bad (ik x) (l3_state.bad x); analz (ik x) \<subseteq> synth (analz (ik x \<inter> payload \<union> ik x \<inter> valid \<union> ik x \<inter> range LtK \<union> Tags)); implAuth A B M \<in> synth (analz (ik x)); M \<in> payload; implAuth A B M \<notin> ik x\<rbrakk> \<Longrightarrow> M \<in> synth (analz (ik x))
 2. \<And>x A B M. \<lbrakk>x \<in> l3_inv4; Keys_bad (ik x) (l3_state.bad x); analz (ik x) \<subseteq> synth (analz (ik x \<inter> payload \<union> ik x \<inter> valid \<union> ik x \<inter> range LtK \<union> Tags)); implAuth A B M \<in> synth (analz (ik x)); M \<in> payload; implAuth A B M \<notin> ik x; B \<notin> l3_state.bad x\<rbrakk> \<Longrightarrow> A \<in> l3_state.bad x
[PROOF STEP]
apply (drule synth_mono, simp, drule subsetD, assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x A B M. \<lbrakk>x \<in> l3_inv4; Keys_bad (ik x) (l3_state.bad x); implAuth A B M \<in> synth (analz (ik x)); M \<in> payload; implAuth A B M \<notin> ik x; implAuth A B M \<in> synth (analz (ik x \<inter> payload \<union> ik x \<inter> valid \<union> ik x \<inter> range LtK \<union> Tags))\<rbrakk> \<Longrightarrow> M \<in> synth (analz (ik x))
 2. \<And>x A B M. \<lbrakk>x \<in> l3_inv4; Keys_bad (ik x) (l3_state.bad x); analz (ik x) \<subseteq> synth (analz (ik x \<inter> payload \<union> ik x \<inter> valid \<union> ik x \<inter> range LtK \<union> Tags)); implAuth A B M \<in> synth (analz (ik x)); M \<in> payload; implAuth A B M \<notin> ik x; B \<notin> l3_state.bad x\<rbrakk> \<Longrightarrow> A \<in> l3_state.bad x
[PROOF STEP]
apply (auto dest!: implAuth_synth_analz [rotated 1, where H="_ \<union> _"] elim!: synth_analz_monotone)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x A B M. \<lbrakk>x \<in> l3_inv4; Keys_bad (ik x) (l3_state.bad x); analz (ik x) \<subseteq> synth (analz (ik x \<inter> payload \<union> ik x \<inter> valid \<union> ik x \<inter> range LtK \<union> Tags)); implAuth A B M \<in> synth (analz (ik x)); M \<in> payload; implAuth A B M \<notin> ik x; B \<notin> l3_state.bad x\<rbrakk> \<Longrightarrow> A \<in> l3_state.bad x
[PROOF STEP]
apply (drule synth_mono, simp, drule subsetD, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x A B M. \<lbrakk>x \<in> l3_inv4; Keys_bad (ik x) (l3_state.bad x); implAuth A B M \<in> synth (analz (ik x)); M \<in> payload; implAuth A B M \<notin> ik x; B \<notin> l3_state.bad x; implAuth A B M \<in> synth (analz (ik x \<inter> payload \<union> ik x \<inter> valid \<union> ik x \<inter> range LtK \<union> Tags))\<rbrakk> \<Longrightarrow> A \<in> l3_state.bad x
[PROOF STEP]
apply (auto dest!: implAuth_synth_analz [rotated 1, where H="_ \<union> _"] elim!: synth_analz_monotone)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma beta_eta_appR[intro]: "t \<rightarrow>\<^sub>\<beta>\<^sub>\<eta>\<^sup>* t' \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sub>\<eta>\<^sup>* s \<degree> t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<rightarrow>\<^sub>\<beta>\<^sub>\<eta>\<^sup>* t' \<Longrightarrow> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sub>\<eta>\<^sup>* s \<degree> t'
[PROOF STEP]
by (induction set: rtranclp) (auto intro: rtranclp.rtrancl_into_rtrancl)


[STATEMENT]
lemma carr_Ssegment_adjunct_ord:"\<lbrakk>Order D; a \<notin> carrier D\<rbrakk> \<Longrightarrow>
                 carrier D = (Ssegment (adjunct_ord D a) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Order D; a \<notin> carrier D\<rbrakk> \<Longrightarrow> carrier D = Ssegment (adjunct_ord D a) a
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Order D; a \<notin> carrier D\<rbrakk> \<Longrightarrow> carrier D \<subseteq> Ssegment (adjunct_ord D a) a
 2. \<lbrakk>Order D; a \<notin> carrier D\<rbrakk> \<Longrightarrow> Ssegment (adjunct_ord D a) a \<subseteq> carrier D
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Order D; a \<notin> carrier D; x \<in> carrier D\<rbrakk> \<Longrightarrow> x \<in> Ssegment (adjunct_ord D a) a
 2. \<lbrakk>Order D; a \<notin> carrier D\<rbrakk> \<Longrightarrow> Ssegment (adjunct_ord D a) a \<subseteq> carrier D
[PROOF STEP]
apply (simp add:Ssegment_def Order.carrier_adjunct_ord)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Order D; a \<notin> carrier D; x \<in> carrier D\<rbrakk> \<Longrightarrow> x \<prec>\<^bsub>adjunct_ord D a\<^esub> a
 2. \<lbrakk>Order D; a \<notin> carrier D\<rbrakk> \<Longrightarrow> Ssegment (adjunct_ord D a) a \<subseteq> carrier D
[PROOF STEP]
apply (simp add:Order.adjunct_ord_large_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Order D; a \<notin> carrier D\<rbrakk> \<Longrightarrow> Ssegment (adjunct_ord D a) a \<subseteq> carrier D
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Order D; a \<notin> carrier D; x \<in> Ssegment (adjunct_ord D a) a\<rbrakk> \<Longrightarrow> x \<in> carrier D
[PROOF STEP]
apply (simp add:Ssegment_def Order.carrier_adjunct_ord)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Order D; a \<notin> carrier D; x \<prec>\<^bsub>adjunct_ord D a\<^esub> a \<and> (x = a \<or> x \<in> carrier D)\<rbrakk> \<Longrightarrow> x \<in> carrier D
[PROOF STEP]
apply (erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Order D; a \<notin> carrier D; x \<prec>\<^bsub>adjunct_ord D a\<^esub> a; x = a \<or> x \<in> carrier D\<rbrakk> \<Longrightarrow> x \<in> carrier D
[PROOF STEP]
apply (erule disjE, simp add:oless_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Order D; a \<notin> carrier D; x \<prec>\<^bsub>adjunct_ord D a\<^esub> a; x \<in> carrier D\<rbrakk> \<Longrightarrow> x \<in> carrier D
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i0_h_pat: "i0.h x y = x+i0.k y+i0.i x y+i0.j x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i0.h x y = x + i0.k y + i5.i x y + i0.j x y
[PROOF STEP]
unfolding i0.h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + x + i0.k y + i5.i x y + i0.j x y = x + i0.k y + i5.i x y + i0.j x y
[PROOF STEP]
by auto


[STATEMENT]
lemma parallel_beta_reduces_equivalent:
  shows "(A >>\<^sup>* B) = (A \<rightarrow>\<beta>\<^sup>* B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A >>\<^sup>* B = A \<rightarrow>\<beta>\<^sup>* B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A >>\<^sup>* B = A \<rightarrow>\<beta>\<^sup>* B
[PROOF STEP]
have \<rightarrow>: "(A >>\<^sup>* B) \<Longrightarrow> (A \<rightarrow>\<beta>\<^sup>* B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A >>\<^sup>* B \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* B
[PROOF STEP]
proof(induction rule: parallel_reduces.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. A \<rightarrow>\<beta>\<^sup>* A
 2. \<And>A A' A''. \<lbrakk>A >>\<^sup>* A'; A \<rightarrow>\<beta>\<^sup>* A'; A' >> A''\<rbrakk> \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* A''
[PROOF STEP]
case (reflexive A)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>A. A \<rightarrow>\<beta>\<^sup>* A
 2. \<And>A A' A''. \<lbrakk>A >>\<^sup>* A'; A \<rightarrow>\<beta>\<^sup>* A'; A' >> A''\<rbrakk> \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* A''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<rightarrow>\<beta>\<^sup>* A
[PROOF STEP]
using beta_reduces.reflexive
[PROOF STATE]
proof (prove)
using this:
?M \<rightarrow>\<beta>\<^sup>* ?M

goal (1 subgoal):
 1. A \<rightarrow>\<beta>\<^sup>* A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A \<rightarrow>\<beta>\<^sup>* A

goal (1 subgoal):
 1. \<And>A A' A''. \<lbrakk>A >>\<^sup>* A'; A \<rightarrow>\<beta>\<^sup>* A'; A' >> A''\<rbrakk> \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* A''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A A' A''. \<lbrakk>A >>\<^sup>* A'; A \<rightarrow>\<beta>\<^sup>* A'; A' >> A''\<rbrakk> \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* A''
[PROOF STEP]
case (transitive A A' A'')
[PROOF STATE]
proof (state)
this:
A >>\<^sup>* A'
A' >> A''
A \<rightarrow>\<beta>\<^sup>* A'

goal (1 subgoal):
 1. \<And>A A' A''. \<lbrakk>A >>\<^sup>* A'; A \<rightarrow>\<beta>\<^sup>* A'; A' >> A''\<rbrakk> \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* A''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A >>\<^sup>* A'
A' >> A''
A \<rightarrow>\<beta>\<^sup>* A'

goal (1 subgoal):
 1. A \<rightarrow>\<beta>\<^sup>* A''
[PROOF STEP]
using beta_reduces_composition parallel_reduction_is_beta_reduction
[PROOF STATE]
proof (prove)
using this:
A >>\<^sup>* A'
A' >> A''
A \<rightarrow>\<beta>\<^sup>* A'
\<lbrakk>?A' \<rightarrow>\<beta>\<^sup>* ?A''; ?A \<rightarrow>\<beta>\<^sup>* ?A'\<rbrakk> \<Longrightarrow> ?A \<rightarrow>\<beta>\<^sup>* ?A''
?A >> ?B \<Longrightarrow> ?A \<rightarrow>\<beta>\<^sup>* ?B

goal (1 subgoal):
 1. A \<rightarrow>\<beta>\<^sup>* A''
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
A \<rightarrow>\<beta>\<^sup>* A''

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A >>\<^sup>* B \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* B

goal (1 subgoal):
 1. A >>\<^sup>* B = A \<rightarrow>\<beta>\<^sup>* B
[PROOF STEP]
have \<leftarrow>: "(A \<rightarrow>\<beta>\<^sup>* B) \<Longrightarrow> (A >>\<^sup>* B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<rightarrow>\<beta>\<^sup>* B \<Longrightarrow> A >>\<^sup>* B
[PROOF STEP]
proof(induction rule: beta_reduces.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M. M >>\<^sup>* M
 2. \<And>M M' M''. \<lbrakk>M \<rightarrow>\<beta>\<^sup>* M'; M >>\<^sup>* M'; M' \<rightarrow>\<beta> M''\<rbrakk> \<Longrightarrow> M >>\<^sup>* M''
[PROOF STEP]
case (reflexive A)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>M. M >>\<^sup>* M
 2. \<And>M M' M''. \<lbrakk>M \<rightarrow>\<beta>\<^sup>* M'; M >>\<^sup>* M'; M' \<rightarrow>\<beta> M''\<rbrakk> \<Longrightarrow> M >>\<^sup>* M''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A >>\<^sup>* A
[PROOF STEP]
using parallel_reduces.reflexive
[PROOF STATE]
proof (prove)
using this:
?A >>\<^sup>* ?A

goal (1 subgoal):
 1. A >>\<^sup>* A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A >>\<^sup>* A

goal (1 subgoal):
 1. \<And>M M' M''. \<lbrakk>M \<rightarrow>\<beta>\<^sup>* M'; M >>\<^sup>* M'; M' \<rightarrow>\<beta> M''\<rbrakk> \<Longrightarrow> M >>\<^sup>* M''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M M' M''. \<lbrakk>M \<rightarrow>\<beta>\<^sup>* M'; M >>\<^sup>* M'; M' \<rightarrow>\<beta> M''\<rbrakk> \<Longrightarrow> M >>\<^sup>* M''
[PROOF STEP]
case (transitive A A' A'')
[PROOF STATE]
proof (state)
this:
A \<rightarrow>\<beta>\<^sup>* A'
A' \<rightarrow>\<beta> A''
A >>\<^sup>* A'

goal (1 subgoal):
 1. \<And>M M' M''. \<lbrakk>M \<rightarrow>\<beta>\<^sup>* M'; M >>\<^sup>* M'; M' \<rightarrow>\<beta> M''\<rbrakk> \<Longrightarrow> M >>\<^sup>* M''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<rightarrow>\<beta>\<^sup>* A'
A' \<rightarrow>\<beta> A''
A >>\<^sup>* A'

goal (1 subgoal):
 1. A >>\<^sup>* A''
[PROOF STEP]
using parallel_reduces.transitive beta_reduction_is_parallel_reduction
[PROOF STATE]
proof (prove)
using this:
A \<rightarrow>\<beta>\<^sup>* A'
A' \<rightarrow>\<beta> A''
A >>\<^sup>* A'
\<lbrakk>?A >>\<^sup>* ?A'; ?A' >> ?A''\<rbrakk> \<Longrightarrow> ?A >>\<^sup>* ?A''
?A \<rightarrow>\<beta> ?B \<Longrightarrow> ?A >> ?B

goal (1 subgoal):
 1. A >>\<^sup>* A''
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
A >>\<^sup>* A''

goal:
No subgoals!
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<rightarrow>\<beta>\<^sup>* B \<Longrightarrow> A >>\<^sup>* B

goal (1 subgoal):
 1. A >>\<^sup>* B = A \<rightarrow>\<beta>\<^sup>* B
[PROOF STEP]
from \<leftarrow>\<rightarrow>
[PROOF STATE]
proof (chain)
picking this:
A \<rightarrow>\<beta>\<^sup>* B \<Longrightarrow> A >>\<^sup>* B
A >>\<^sup>* B \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* B
[PROOF STEP]
show "(A >>\<^sup>* B) = (A \<rightarrow>\<beta>\<^sup>* B)"
[PROOF STATE]
proof (prove)
using this:
A \<rightarrow>\<beta>\<^sup>* B \<Longrightarrow> A >>\<^sup>* B
A >>\<^sup>* B \<Longrightarrow> A \<rightarrow>\<beta>\<^sup>* B

goal (1 subgoal):
 1. A >>\<^sup>* B = A \<rightarrow>\<beta>\<^sup>* B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A >>\<^sup>* B = A \<rightarrow>\<beta>\<^sup>* B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma triangle:
  "turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z
[PROOF STEP]
have "turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e" if "e > 0" for e
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
have "Inf {(\<Sum> i \<in> {0..<n}. f (u i) (u (Suc i)))| u (n::nat). u 0 = x \<and> u n = y} < turn_into_distance f x y + e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y} < turn_into_distance f x y + e / 2
[PROOF STEP]
unfolding turn_into_distance_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y} < Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y} + e / 2
[PROOF STEP]
using \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < e

goal (1 subgoal):
 1. Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y} < Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y} + e / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y} < turn_into_distance f x y + e / 2

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y} < turn_into_distance f x y + e / 2
[PROOF STEP]
have "\<exists>a \<in> {(\<Sum> i \<in> {0..<n}. f (u i) (u (Suc i)))| u (n::nat). u 0 = x \<and> u n = y}. a < turn_into_distance f x y + e/2"
[PROOF STATE]
proof (prove)
using this:
Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y} < turn_into_distance f x y + e / 2

goal (1 subgoal):
 1. \<exists>a\<in>{\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y}. a < turn_into_distance f x y + e / 2
[PROOF STEP]
by (rule cInf_lessD[OF nonempty])
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>{\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y}. a < turn_into_distance f x y + e / 2

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a\<in>{\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y}. a < turn_into_distance f x y + e / 2
[PROOF STEP]
obtain u n where U: "u 0 = x" "u n = y" "(\<Sum> i \<in> {0..<n}. f (u i) (u (Suc i))) < turn_into_distance f x y + e/2"
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>{\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = y}. a < turn_into_distance f x y + e / 2

goal (1 subgoal):
 1. (\<And>u n. \<lbrakk>u 0 = x; u n = y; (\<Sum>i = 0..<n. f (u i) (u (Suc i))) < turn_into_distance f x y + e / 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u 0 = x
u n = y
(\<Sum>i = 0..<n. f (u i) (u (Suc i))) < turn_into_distance f x y + e / 2

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
have "Inf {(\<Sum> i \<in> {0..<m}. f (v i) (v (Suc i)))| v (m::nat). v 0 = y \<and> v m = z} < turn_into_distance f y z + e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z} < turn_into_distance f y z + e / 2
[PROOF STEP]
unfolding turn_into_distance_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z} < Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = y \<and> u n = z} + e / 2
[PROOF STEP]
using \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < e

goal (1 subgoal):
 1. Inf {\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z} < Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = y \<and> u n = z} + e / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Inf {\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z} < turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inf {\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z} < turn_into_distance f y z + e / 2
[PROOF STEP]
have "\<exists>a \<in> {(\<Sum> i \<in> {0..<m}. f (v i) (v (Suc i)))| v (m::nat). v 0 = y \<and> v m = z}. a < turn_into_distance f y z + e/2"
[PROOF STATE]
proof (prove)
using this:
Inf {\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z} < turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. \<exists>a\<in>{\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z}. a < turn_into_distance f y z + e / 2
[PROOF STEP]
by (rule cInf_lessD[OF nonempty])
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>{\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z}. a < turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a\<in>{\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z}. a < turn_into_distance f y z + e / 2
[PROOF STEP]
obtain v m where V: "v 0 = y" "v m = z" "(\<Sum> i \<in> {0..<m}. f (v i) (v (Suc i))) < turn_into_distance f y z + e/2"
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>{\<Sum>i = 0..<m. f (v i) (v (Suc i)) |v m. v 0 = y \<and> v m = z}. a < turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. (\<And>v m. \<lbrakk>v 0 = y; v m = z; (\<Sum>i = 0..<m. f (v i) (v (Suc i))) < turn_into_distance f y z + e / 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v 0 = y
v m = z
(\<Sum>i = 0..<m. f (v i) (v (Suc i))) < turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
define w where "w = (\<lambda>i. if i < n then u i else v (i-n))"
[PROOF STATE]
proof (state)
this:
w = (\<lambda>i. if i < n then u i else v (i - n))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
have *: "w 0 = x" "w (n+m) = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w 0 = x &&& w (n + m) = z
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 < n then u 0 else v (0 - n)) = x &&& (if n + m < n then u (n + m) else v (n + m - n)) = z
[PROOF STEP]
using U V
[PROOF STATE]
proof (prove)
using this:
u 0 = x
u n = y
(\<Sum>i = 0..<n. f (u i) (u (Suc i))) < turn_into_distance f x y + e / 2
v 0 = y
v m = z
(\<Sum>i = 0..<m. f (v i) (v (Suc i))) < turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. (if 0 < n then u 0 else v (0 - n)) = x &&& (if n + m < n then u (n + m) else v (n + m - n)) = z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w 0 = x
w (n + m) = z

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
have "turn_into_distance f x z \<le> (\<Sum>i = 0..<n+m. f (w i) (w (Suc i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. turn_into_distance f x z \<le> (\<Sum>i = 0..<n + m. f (w i) (w (Suc i)))
[PROOF STEP]
unfolding turn_into_distance_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = z} \<le> (\<Sum>i = 0..<n + m. f (w i) (w (Suc i)))
[PROOF STEP]
apply (rule cInf_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<Sum>i = 0..<n + m. f (w i) (w (Suc i))) \<in> {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = z}
 2. bdd_below {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = z}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
w 0 = x
w (n + m) = z

goal (2 subgoals):
 1. (\<Sum>i = 0..<n + m. f (w i) (w (Suc i))) \<in> {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = z}
 2. bdd_below {\<Sum>i = 0..<n. f (u i) (u (Suc i)) |u n. u 0 = x \<and> u n = z}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
turn_into_distance f x z \<le> (\<Sum>i = 0..<n + m. f (w i) (w (Suc i)))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
turn_into_distance f x z \<le> (\<Sum>i = 0..<n + m. f (w i) (w (Suc i)))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
have "... = (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = n..<n+m. f (w i) (w (Suc i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n + m. f (w i) (w (Suc i))) = (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = n..<n + m. f (w i) (w (Suc i)))
[PROOF STEP]
by (simp add: sum.atLeastLessThan_concat)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n + m. f (w i) (w (Suc i))) = (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = n..<n + m. f (w i) (w (Suc i)))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n + m. f (w i) (w (Suc i))) = (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = n..<n + m. f (w i) (w (Suc i)))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
have "... = (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = 0..<m. f (w (i+n)) (w (Suc (i+n))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = n..<n + m. f (w i) (w (Suc i))) = (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = 0..<m. f (w (i + n)) (w (Suc (i + n))))
[PROOF STEP]
by (auto intro!: sum.reindex_bij_betw[symmetric] bij_betw_byWitness[of _ "\<lambda>i. i-n"])
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = n..<n + m. f (w i) (w (Suc i))) = (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = 0..<m. f (w (i + n)) (w (Suc (i + n))))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = n..<n + m. f (w i) (w (Suc i))) = (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = 0..<m. f (w (i + n)) (w (Suc (i + n))))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
have "... = (\<Sum>i = 0..<n. f (u i) (u (Suc i))) + (\<Sum>i = 0..<m. f (v i) (v (Suc i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = 0..<m. f (w (i + n)) (w (Suc (i + n)))) = (\<Sum>i = 0..<n. f (u i) (u (Suc i))) + (\<Sum>i = 0..<m. f (v i) (v (Suc i)))
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. f (if i < n then u i else v (i - n)) (if Suc i < n then u (Suc i) else v (Suc i - n))) + (\<Sum>i = 0..<m. f (if i + n < n then u (i + n) else v (i + n - n)) (if Suc (i + n) < n then u (Suc (i + n)) else v (Suc (i + n) - n))) = (\<Sum>i = 0..<n. f (u i) (u (Suc i))) + (\<Sum>i = 0..<m. f (v i) (v (Suc i)))
[PROOF STEP]
apply (auto intro!: sum.cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < n; \<not> Suc x < n\<rbrakk> \<Longrightarrow> f (u x) (v 0) = f (u x) (u (Suc x))
[PROOF STEP]
using U(2) V(1) Suc_lessI
[PROOF STATE]
proof (prove)
using this:
u n = y
v 0 = y
\<lbrakk>?m < ?n; Suc ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> Suc ?m < ?n

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x < n; \<not> Suc x < n\<rbrakk> \<Longrightarrow> f (u x) (v 0) = f (u x) (u (Suc x))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = 0..<m. f (w (i + n)) (w (Suc (i + n)))) = (\<Sum>i = 0..<n. f (u i) (u (Suc i))) + (\<Sum>i = 0..<m. f (v i) (v (Suc i)))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. f (w i) (w (Suc i))) + (\<Sum>i = 0..<m. f (w (i + n)) (w (Suc (i + n)))) = (\<Sum>i = 0..<n. f (u i) (u (Suc i))) + (\<Sum>i = 0..<m. f (v i) (v (Suc i)))

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
have "... < turn_into_distance f x y + e/2 + turn_into_distance f y z + e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<n. f (u i) (u (Suc i))) + (\<Sum>i = 0..<m. f (v i) (v (Suc i))) < turn_into_distance f x y + e / 2 + turn_into_distance f y z + e / 2
[PROOF STEP]
using U(3) V(3)
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<n. f (u i) (u (Suc i))) < turn_into_distance f x y + e / 2
(\<Sum>i = 0..<m. f (v i) (v (Suc i))) < turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. (\<Sum>i = 0..<n. f (u i) (u (Suc i))) + (\<Sum>i = 0..<m. f (v i) (v (Suc i))) < turn_into_distance f x y + e / 2 + turn_into_distance f y z + e / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<n. f (u i) (u (Suc i))) + (\<Sum>i = 0..<m. f (v i) (v (Suc i))) < turn_into_distance f x y + e / 2 + turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
turn_into_distance f x z < turn_into_distance f x y + e / 2 + turn_into_distance f y z + e / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
turn_into_distance f x z < turn_into_distance f x y + e / 2 + turn_into_distance f y z + e / 2

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < ?e \<Longrightarrow> turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + ?e

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?e \<Longrightarrow> turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + ?e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + ?e

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z
[PROOF STEP]
using field_le_epsilon
[PROOF STATE]
proof (prove)
using this:
0 < ?e \<Longrightarrow> turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z + ?e
(\<And>e. (0::?'a) < e \<Longrightarrow> ?x \<le> ?y + e) \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
turn_into_distance f x z \<le> turn_into_distance f x y + turn_into_distance f y z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ta_prod_rta:
  assumes TA: "ranked_tree_automaton TA1 A" "ranked_tree_automaton TA2 A"
  shows "ranked_tree_automaton (ta_prod TA1 TA2) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ranked_tree_automaton (ta_prod TA1 TA2) A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ranked_tree_automaton (ta_prod TA1 TA2) A
[PROOF STEP]
interpret ta1: ranked_tree_automaton TA1 A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ranked_tree_automaton TA1 A
[PROOF STEP]
using TA
[PROOF STATE]
proof (prove)
using this:
ranked_tree_automaton TA1 A
ranked_tree_automaton TA2 A

goal (1 subgoal):
 1. ranked_tree_automaton TA1 A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ranked_tree_automaton (ta_prod TA1 TA2) A
[PROOF STEP]
interpret ta2: ranked_tree_automaton TA2 A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ranked_tree_automaton TA2 A
[PROOF STEP]
using TA
[PROOF STATE]
proof (prove)
using this:
ranked_tree_automaton TA1 A
ranked_tree_automaton TA2 A

goal (1 subgoal):
 1. ranked_tree_automaton TA2 A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ranked_tree_automaton (ta_prod TA1 TA2) A
[PROOF STEP]
interpret tap: tree_automaton "(ta_prod TA1 TA2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tree_automaton (ta_prod TA1 TA2)
[PROOF STEP]
apply (rule ta_prod_correct_aux2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. tree_automaton TA1
 2. tree_automaton TA2
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ranked_tree_automaton (ta_prod TA1 TA2) A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ranked_tree_automaton (ta_prod TA1 TA2) A
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q f qs. q \<rightarrow> f qs \<in> tap.\<delta> \<Longrightarrow> A f = Some (length qs)
[PROOF STEP]
apply (unfold ta_prod_def \<delta>_prod_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q f qs. q \<rightarrow> f qs \<in> ta_rules \<lparr>ta_initial = ta1.Qi \<times> ta2.Qi, ta_rules = {r_prod q1 \<rightarrow> l qs1 q2 \<rightarrow> l qs2 |q1 q2 l qs1 qs2. length qs1 = length qs2 \<and> q1 \<rightarrow> l qs1 \<in> ta1.\<delta> \<and> q2 \<rightarrow> l qs2 \<in> ta2.\<delta>}\<rparr> \<Longrightarrow> A f = Some (length qs)
[PROOF STEP]
apply (auto intro: ta1.ranked ta2.ranked)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ranked_tree_automaton (ta_prod TA1 TA2) A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DynCastFail':
  "\<lbrakk> P,E \<turnstile> \<langle>e,s\<^sub>0\<rangle>\<Rightarrow>' \<langle>ref (a,Cs),(h,l)\<rangle>; h a = Some(D,S); \<not> P \<turnstile> Path D to C unique;
    \<not> P \<turnstile> Path last Cs to C unique; C \<notin> set Cs \<rbrakk>
  \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<^sub>0\<rangle> \<Rightarrow>' \<langle>null,(h,l)\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,E \<turnstile> \<langle>e,s\<^sub>0\<rangle> \<Rightarrow>' \<langle>ref (a, Cs),(h, l)\<rangle>; h a = \<lfloor>(D, S)\<rfloor>; \<not> P \<turnstile> Path D to C unique; \<not> P \<turnstile> Path last Cs to C unique; C \<notin> set Cs\<rbrakk> \<Longrightarrow> P,E \<turnstile> \<langle>Cast C e,s\<^sub>0\<rangle> \<Rightarrow>' \<langle>null,(h, l)\<rangle>
[PROOF STEP]
by transfer(rule DynCastFail)


[STATEMENT]
lemma S_M_grounding_of_clss:
  assumes "C \<in> grounding_of_clss M"
  obtains D \<sigma> where
    "D \<in> M \<and> C = D \<cdot> \<sigma> \<and> S_M C = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> S_M C = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (atomize_elim, unfold S_M_def eqTrueI[OF assms] if_True, rule someI_ex)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> x = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
C \<in> grounding_of_clss M
[PROOF STEP]
show "\<exists>C' D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> C' = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>"
[PROOF STATE]
proof (prove)
using this:
C \<in> grounding_of_clss M

goal (1 subgoal):
 1. \<exists>C' D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> C' = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>
[PROOF STEP]
by (auto simp: grounding_of_clss_def grounding_of_cls_def)
[PROOF STATE]
proof (state)
this:
\<exists>C' D \<sigma>. D \<in> M \<and> C = D \<cdot> \<sigma> \<and> C' = S D \<cdot> \<sigma> \<and> is_ground_subst \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cf_comp_assoc[cat_cs_simps]:
  assumes "\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
" and "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "(\<HH> \<circ>\<^sub>C\<^sub>F \<GG>) \<circ>\<^sub>C\<^sub>F \<FF> = \<HH> \<circ>\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>C\<^sub>F \<FF>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
proof(rule cf_eqI[of \<alpha> \<AA> \
 _ \<AA> \
])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>
 5. \<AA> = \<AA>
 6. \
 = \

[PROOF STEP]
interpret \<HH>: is_functor \<alpha> \<CC> \
 \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>
 5. \<AA> = \<AA>
 6. \
 = \

[PROOF STEP]
interpret \<GG>: is_functor \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>
 5. \<AA> = \<AA>
 6. \
 = \

[PROOF STEP]
interpret \<FF>: is_functor \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>
 5. \<AA> = \<AA>
 6. \
 = \

[PROOF STEP]
from \<FF>.is_functor_axioms \<GG>.is_functor_axioms \<HH>.is_functor_axioms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
show "\<HH> \<circ>\<^sub>C\<^sub>F (\<GG> \<circ>\<^sub>C\<^sub>F \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
" and "\<HH> \<circ>\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>C\<^sub>F \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \
 &&& \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (auto simp: cat_cs_simps intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal (4 subgoals):
 1. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>
 2. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>
 3. \<AA> = \<AA>
 4. \
 = \

[PROOF STEP]
qed (simp_all add: dghm_comp_components vcomp_assoc)


[STATEMENT]
lemma (in is_functor) cf_cf_comp_cf_id_right[cat_cs_simps]: "\<FF> \<circ>\<^sub>C\<^sub>F cf_id \<AA> = \<FF>"
  \<comment>\<open>See Chapter I-3 in \cite{mac_lane_categories_2010}).\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> = \<FF>
[PROOF STEP]
by
    (
      rule cf_eqI,
      unfold dghm_id_components dghm_comp_components dghm_id_components
    )
    (
      auto
        intro: cat_cs_intros
        simp: cat_cs_simps cf_ArrMap_vrange cf_ObjMap_vrange
    )


[STATEMENT]
lemma schroeder_top:
  "x * top \<le> y \<longleftrightarrow> -y * top \<le> -x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * top \<le> y) = (- y * top \<le> - x)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x * top \<le> y \<Longrightarrow> - y * top \<le> - x
 2. - y * top \<le> - x \<Longrightarrow> x * top \<le> y
[PROOF STEP]
using compl_mono inf.order_trans mult_left_isotone schroeder_top_sub
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> - ?y \<le> - ?x
\<lbrakk>?y \<le> ?x; ?z \<le> ?y\<rbrakk> \<Longrightarrow> ?z \<le> ?x
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
- (?x * top) * top \<le> - ?x

goal (2 subgoals):
 1. x * top \<le> y \<Longrightarrow> - y * top \<le> - x
 2. - y * top \<le> - x \<Longrightarrow> x * top \<le> y
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - y * top \<le> - x \<Longrightarrow> x * top \<le> y
[PROOF STEP]
by (metis compl_mono double_compl mult_left_isotone order_trans schroeder_top_sub)