[STATEMENT]
lemma local_flow_tank: "local_flow (f k) UNIV UNIV (\<phi> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local_flow (f k) UNIV UNIV (\<phi> k)
[PROOF STEP]
apply (unfold_locales, unfold local_lipschitz_def lipschitz_on_def, simp_all, clarsimp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t. \<exists>u>0. (\<exists>ta. dist t ta \<le> u) \<longrightarrow> (\<exists>L\<ge>0. \<forall>xa\<in>cball x u. \<forall>y\<in>cball x u. 0 \<le> L \<cdot> dist xa y)
 2. \<And>t s. \<forall>i. (i = 1 \<longrightarrow>  D (\<lambda>x. k \<cdot> x + s $ 1) = (\<lambda>x. k) on {0--t}) \<and> (i \<noteq> 1 \<longrightarrow> (i = 2 \<longrightarrow>  D (\<lambda>x. x + s $ 2) = (\<lambda>x. 1) on {0--t}) \<and> (i \<noteq> 2 \<longrightarrow>  D (\<lambda>x. s $ i) = (\<lambda>x. 0) on {0--t}))
 3. \<And>s. \<phi> k 0 s = s
[PROOF STEP]
apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. dist t ta \<cdot> 2 \<le> 1 \<Longrightarrow> 0 \<le> 1 \<and> (\<forall>xa\<in>cball x (1 / 2). \<forall>y\<in>cball x (1 / 2). 0 \<le> 1 \<cdot> dist xa y)
 2. \<And>t s. \<forall>i. (i = 1 \<longrightarrow>  D (\<lambda>x. k \<cdot> x + s $ 1) = (\<lambda>x. k) on {0--t}) \<and> (i \<noteq> 1 \<longrightarrow> (i = 2 \<longrightarrow>  D (\<lambda>x. x + s $ 2) = (\<lambda>x. 1) on {0--t}) \<and> (i \<noteq> 2 \<longrightarrow>  D (\<lambda>x. s $ i) = (\<lambda>x. 0) on {0--t}))
 3. \<And>s. \<phi> k 0 s = s
[PROOF STEP]
apply(simp add: dist_norm norm_vec_def L2_set_def, unfold UNIV_4)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. \<bar>t - ta\<bar> \<cdot> 2 \<le> 1 \<Longrightarrow> \<forall>xa\<in>cball x (1 / 2). \<forall>y\<in>cball x (1 / 2). 0 \<le> (\<Sum>i\<in>insert 1 (insert 2 (insert 3 (\<eta> 4))). (xa $ i - y $ i)\<^sup>2)
 2. \<And>t s. \<forall>i. (i = 1 \<longrightarrow>  D (\<lambda>x. k \<cdot> x + s $ 1) = (\<lambda>x. k) on {0--t}) \<and> (i \<noteq> 1 \<longrightarrow> (i = 2 \<longrightarrow>  D (\<lambda>x. x + s $ 2) = (\<lambda>x. 1) on {0--t}) \<and> (i \<noteq> 2 \<longrightarrow>  D (\<lambda>x. s $ i) = (\<lambda>x. 0) on {0--t}))
 3. \<And>s. \<phi> k 0 s = s
[PROOF STEP]
by (auto intro!: poly_derivatives simp: vec_eq_iff)