[STATEMENT]
lemma enumerate_suc: \<open>enumerate (Suc n) l = map (\<lambda> (a,b). (a+1::nat,b)) (enumerate n l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enumerate (Suc n) l = map (\<lambda>(a, b). (a + 1, b)) (enumerate n l)
[PROOF STEP]
proof (induction \<open>l\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enumerate (Suc n) [] = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n [])
 2. \<And>a l. enumerate (Suc n) l = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n l) \<Longrightarrow> enumerate (Suc n) (a # l) = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n (a # l))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. enumerate (Suc n) [] = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n [])
 2. \<And>a l. enumerate (Suc n) l = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n l) \<Longrightarrow> enumerate (Suc n) (a # l) = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n (a # l))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enumerate (Suc n) [] = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enumerate (Suc n) [] = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n [])

goal (1 subgoal):
 1. \<And>a l. enumerate (Suc n) l = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n l) \<Longrightarrow> enumerate (Suc n) (a # l) = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n (a # l))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. enumerate (Suc n) l = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n l) \<Longrightarrow> enumerate (Suc n) (a # l) = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n (a # l))
[PROOF STEP]
case (Cons a x)
[PROOF STATE]
proof (state)
this:
enumerate (Suc n) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n x)

goal (1 subgoal):
 1. \<And>a l. enumerate (Suc n) l = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n l) \<Longrightarrow> enumerate (Suc n) (a # l) = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n (a # l))
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
enumerate (Suc n) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n x)

goal (1 subgoal):
 1. \<And>a l. enumerate (Suc n) l = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n l) \<Longrightarrow> enumerate (Suc n) (a # l) = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n (a # l))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enumerate (Suc n) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
enumerate (Suc n) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n x)

goal (1 subgoal):
 1. enumerate (Suc n) (a # x) = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n (a # x))
[PROOF STEP]
apply(simp only:enumerate_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enumerate (Suc n) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n x) \<Longrightarrow> (Suc n, a) # enumerate (Suc (Suc n)) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) ((n, a) # map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n x))
[PROOF STEP]
apply(simp only:\<open>enumerate (Suc n) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n x)\<close>[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enumerate (Suc n) x = enumerate (Suc n) x \<Longrightarrow> (Suc n, a) # enumerate (Suc (Suc n)) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) ((n, a) # enumerate (Suc n) x)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enumerate (Suc (Suc n)) x = map (\<lambda>(a, y). (Suc a, y)) (enumerate (Suc n) x)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
enumerate (Suc n) x = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n x)

goal (1 subgoal):
 1. enumerate (Suc (Suc n)) x = map (\<lambda>(a, y). (Suc a, y)) (enumerate (Suc n) x)
[PROOF STEP]
by (metis apfst_conv cond_case_prod_eta enumerate_Suc_eq)
[PROOF STATE]
proof (state)
this:
enumerate (Suc n) (a # x) = map (\<lambda>a. case a of (a, b) \<Rightarrow> (a + 1, b)) (enumerate n (a # x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_assoc_aux1:
 \<open>(\<lambda>(p, y). 10 ^ p * y) \<circ> (\<lambda>(a, y). (Suc a, y)) = (\<lambda>(p, y). (10::nat) * (10 ^ p) * y)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(p, y). 10 ^ p * y) \<circ> (\<lambda>(a, y). (Suc a, y)) = (\<lambda>(p, y). 10 * 10 ^ p * y)
[PROOF STEP]
by(auto simp:o_def)


[STATEMENT]
lemma fold_map_transfer:
 \<open>(foldr (+) (map (\<lambda>(x,y). 10 * (f (x,y))) l) (0::nat)) = 10 * (foldr (+) (map (\<lambda>x. (f x)) l) (0::nat))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (+) (map (\<lambda>(x, y). 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0
[PROOF STEP]
proof(induct \<open>l\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) []) 0 = 10 * foldr (+) (map f []) 0
 2. \<And>a l. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0 \<Longrightarrow> foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) (a # l)) 0 = 10 * foldr (+) (map f (a # l)) 0
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) []) 0 = 10 * foldr (+) (map f []) 0
 2. \<And>a l. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0 \<Longrightarrow> foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) (a # l)) 0 = 10 * foldr (+) (map f (a # l)) 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) []) 0 = 10 * foldr (+) (map f []) 0
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) []) 0 = 10 * foldr (+) (map f []) 0

goal (1 subgoal):
 1. \<And>a l. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0 \<Longrightarrow> foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) (a # l)) 0 = 10 * foldr (+) (map f (a # l)) 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a l. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0 \<Longrightarrow> foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) (a # l)) 0 = 10 * foldr (+) (map f (a # l)) 0
[PROOF STEP]
case (Cons a l)
[PROOF STATE]
proof (state)
this:
foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0

goal (1 subgoal):
 1. \<And>a l. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0 \<Longrightarrow> foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) (a # l)) 0 = 10 * foldr (+) (map f (a # l)) 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) l) 0 = 10 * foldr (+) (map f l) 0

goal (1 subgoal):
 1. foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) (a # l)) 0 = 10 * foldr (+) (map f (a # l)) 0
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
foldr (+) (map (\<lambda>a. case a of (x, y) \<Rightarrow> 10 * f (x, y)) (a # l)) 0 = 10 * foldr (+) (map f (a # l)) 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_assoc_aux2: \<open>(\<lambda>(p, y). 10 * 10 ^ p * (y::nat)) = (\<lambda>(p, y). 10 * (10 ^ p * y))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(p, y). 10 * 10 ^ p * y) = (\<lambda>(p, y). 10 * (10 ^ p * y))
[PROOF STEP]
by(auto)


[STATEMENT]
lemma nat_implode_explode_id: \<open>nat_implode (nat_explode n) = n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_implode (nat_explode n) = n
[PROOF STEP]
proof (cases \<open>n=0\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> nat_implode (nat_explode n) = n
 2. n \<noteq> 0 \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> nat_implode (nat_explode n) = n
 2. n \<noteq> 0 \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> nat_implode (nat_explode n) = n
 2. n \<noteq> 0 \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. nat_implode (nat_explode n) = n
[PROOF STEP]
by (simp add: nat_explode_def nat_implode_def)
[PROOF STATE]
proof (state)
this:
nat_implode (nat_explode n) = n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. nat_implode (nat_explode n) = n
[PROOF STEP]
proof (induct \<open>n\<close> rule: nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m
n \<noteq> 0

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m
n \<noteq> 0

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m
n \<noteq> 0
[PROOF STEP]
have
      **: \<open>nat_implode (nat_explode (n div 10)) = n div 10\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m
n \<noteq> 0

goal (1 subgoal):
 1. nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
proof (cases \<open>n div 10 = 0\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0; n div 10 = 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode (n div 10)) = n div 10
 2. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0; n div 10 \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n div 10 = 0

goal (2 subgoals):
 1. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0; n div 10 = 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode (n div 10)) = n div 10
 2. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0; n div 10 \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n div 10 = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n div 10 = 0

goal (1 subgoal):
 1. nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
by(simp add: nat_explode_def nat_implode_def)
[PROOF STATE]
proof (state)
this:
nat_implode (nat_explode (n div 10)) = n div 10

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0; n div 10 \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0; n div 10 \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n div 10 \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0; n div 10 \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n div 10 \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n div 10 \<noteq> 0

goal (1 subgoal):
 1. nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
using div_ten_less[of \<open>n\<close>] *
[PROOF STATE]
proof (prove)
using this:
n div 10 \<noteq> 0
n \<noteq> 0 \<Longrightarrow> n div 10 < n
\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m
n \<noteq> 0

goal (1 subgoal):
 1. nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
nat_implode (nat_explode (n div 10)) = n div 10

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nat_implode (nat_explode (n div 10)) = n div 10

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<noteq> 0 \<longrightarrow> nat_implode (nat_explode m) = m; n \<noteq> 0\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_implode (nat_explode (n div 10)) = n div 10
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
nat_implode (nat_explode (n div 10)) = n div 10

goal (1 subgoal):
 1. nat_implode (nat_explode n) = n
[PROOF STEP]
proof (cases \<open>n < 10\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>nat_implode (nat_explode (n div 10)) = n div 10; n < 10\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
 2. \<lbrakk>nat_implode (nat_explode (n div 10)) = n div 10; \<not> n < 10\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n < 10

goal (2 subgoals):
 1. \<lbrakk>nat_implode (nat_explode (n div 10)) = n div 10; n < 10\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
 2. \<lbrakk>nat_implode (nat_explode (n div 10)) = n div 10; \<not> n < 10\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < 10
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n < 10

goal (1 subgoal):
 1. nat_implode (nat_explode n) = n
[PROOF STEP]
by(simp add: nat_explode_def nat_implode_def)
[PROOF STATE]
proof (state)
this:
nat_implode (nat_explode n) = n

goal (1 subgoal):
 1. \<lbrakk>nat_implode (nat_explode (n div 10)) = n div 10; \<not> n < 10\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>nat_implode (nat_explode (n div 10)) = n div 10; \<not> n < 10\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n < 10

goal (1 subgoal):
 1. \<lbrakk>nat_implode (nat_explode (n div 10)) = n div 10; \<not> n < 10\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
note *** = this
[PROOF STATE]
proof (state)
this:
\<not> n < 10

goal (1 subgoal):
 1. \<lbrakk>nat_implode (nat_explode (n div 10)) = n div 10; \<not> n < 10\<rbrakk> \<Longrightarrow> nat_implode (nat_explode n) = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> n < 10
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> n < 10

goal (1 subgoal):
 1. nat_implode (nat_explode n) = n
[PROOF STEP]
apply(simp (no_asm)  add:nat_explode_def del:rev_rev_ident)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> nat_implode (rev (case n < 10 of True \<Rightarrow> [n mod 10] | False \<Rightarrow> n mod 10 # nat_explode' (n div 10))) = n
[PROOF STEP]
apply(simp only: bool.case(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> nat_implode (rev (n mod 10 # nat_explode' (n div 10))) = n
[PROOF STEP]
apply(simp del:nat_explode'.simps rev_rev_ident)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> nat_implode (rev (nat_explode' (n div 10)) @ [n mod 10]) = n
[PROOF STEP]
apply(fold nat_explode_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> nat_implode (nat_explode (n div 10) @ [n mod 10]) = n
[PROOF STEP]
apply(simp only:nat_implode_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> 1 * (n mod 10) + foldr (+) (map (\<lambda>(p, y). 10 ^ p * y) (enumerate (Suc 0) (rev (nat_explode (n div 10))))) 0 = n
[PROOF STEP]
apply(simp add:enumerate_suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> n mod 10 + foldr (+) (map ((\<lambda>(p, y). 10 ^ p * y) \<circ> (\<lambda>(a, y). (Suc a, y))) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = n
[PROOF STEP]
apply(simp only:mult_assoc_aux1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> n mod 10 + foldr (+) (map (\<lambda>(p, y). 10 * 10 ^ p * y) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = n
[PROOF STEP]
using mult_assoc_aux2
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(p, y). 10 * 10 ^ p * y) = (\<lambda>(p, y). 10 * (10 ^ p * y))

goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> n mod 10 + foldr (+) (map (\<lambda>(p, y). 10 * 10 ^ p * y) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = n
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> n < 10; (\<lambda>(p, y). 10 * 10 ^ p * y) = (\<lambda>(p, y). 10 * (10 ^ p * y))\<rbrakk> \<Longrightarrow> n mod 10 + foldr (+) (map (\<lambda>(p, y). 10 * (10 ^ p * y)) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = n
[PROOF STEP]
using fold_map_transfer[of \<open>\<lambda>(p, y). 10 ^ p * y\<close>
                                   \<open>(enumerate 0 (rev (nat_explode (n div 10))))\<close>, simplified]
[PROOF STATE]
proof (prove)
using this:
foldr (+) (map (\<lambda>(x, y). 10 * (10 ^ x * y)) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = 10 * foldr (+) (map (\<lambda>x. case x of (p, y) \<Rightarrow> 10 ^ p * y) (enumerate 0 (rev (nat_explode (n div 10))))) 0

goal (1 subgoal):
 1. \<lbrakk>\<not> n < 10; (\<lambda>(p, y). 10 * 10 ^ p * y) = (\<lambda>(p, y). 10 * (10 ^ p * y))\<rbrakk> \<Longrightarrow> n mod 10 + foldr (+) (map (\<lambda>(p, y). 10 * (10 ^ p * y)) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = n
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> n < 10; (\<lambda>(p, y). 10 * 10 ^ p * y) = (\<lambda>(p, y). 10 * (10 ^ p * y)); foldr (+) (map (\<lambda>(x, y). 10 * (10 ^ x * y)) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = 10 * foldr (+) (map (\<lambda>x. case x of (p, y) \<Rightarrow> 10 ^ p * y) (enumerate 0 (rev (nat_explode (n div 10))))) 0\<rbrakk> \<Longrightarrow> n mod 10 + 10 * foldr (+) (map (\<lambda>p. case p of (p, y) \<Rightarrow> 10 ^ p * y) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = n
[PROOF STEP]
apply(fold nat_implode_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> n < 10; (\<lambda>(p, y). 10 * 10 ^ p * y) = (\<lambda>(p, y). 10 * (10 ^ p * y)); foldr (+) (map (\<lambda>(x, y). 10 * (10 ^ x * y)) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = 10 * nat_implode (nat_explode (n div 10))\<rbrakk> \<Longrightarrow> n mod 10 + 10 * nat_implode (nat_explode (n div 10)) = n
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
nat_implode (nat_explode (n div 10)) = n div 10

goal (1 subgoal):
 1. \<lbrakk>\<not> n < 10; (\<lambda>(p, y). 10 * 10 ^ p * y) = (\<lambda>(p, y). 10 * (10 ^ p * y)); foldr (+) (map (\<lambda>(x, y). 10 * (10 ^ x * y)) (enumerate 0 (rev (nat_explode (n div 10))))) 0 = 10 * nat_implode (nat_explode (n div 10))\<rbrakk> \<Longrightarrow> n mod 10 + 10 * nat_implode (nat_explode (n div 10)) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nat_implode (nat_explode n) = n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nat_implode (nat_explode n) = n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nat_implode (nat_explode n) = n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Show_nat_not_neg:
  \<open>set (Show\<^sub>n\<^sub>a\<^sub>t n) \<subseteq>{CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
                     CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Show\<^sub>n\<^sub>a\<^sub>t n) \<subseteq> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
[PROOF STEP]
unfolding Show\<^sub>n\<^sub>a\<^sub>t_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map digit_of_nat (nat_explode n)) \<subseteq> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
[PROOF STEP]
using  nat_explode_digits[of n]  img_digit_of_nat imageE image_set subsetI
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>set (nat_explode n). d < 10
?n < 10 \<Longrightarrow> digit_of_nat ?n \<in> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
\<lbrakk>?b \<in> ?f ` ?A; \<And>x. \<lbrakk>?b = ?f x; x \<in> ?A\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
?f ` set ?xs = set (map ?f ?xs)
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B

goal (1 subgoal):
 1. set (map digit_of_nat (nat_explode n)) \<subseteq> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
[PROOF STEP]
by (smt (verit) imageE image_set subsetI)


[STATEMENT]
lemma Show_nat_not_empty: \<open>(Show\<^sub>n\<^sub>a\<^sub>t n) \<noteq> []\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Show\<^sub>n\<^sub>a\<^sub>t n \<noteq> []
[PROOF STEP]
by (simp add: Show\<^sub>n\<^sub>a\<^sub>t_def nat_explode_not_empty)


[STATEMENT]
lemma not_hd: \<open>L \<noteq> [] \<Longrightarrow> e \<notin> set(L) \<Longrightarrow> hd L \<noteq> e\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>L \<noteq> []; e \<notin> set L\<rbrakk> \<Longrightarrow> hd L \<noteq> e
[PROOF STEP]
by auto


[STATEMENT]
lemma Show_nat_not_neg'': \<open>hd (Show\<^sub>n\<^sub>a\<^sub>t n) \<noteq> (CHR ''-'')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (Show\<^sub>n\<^sub>a\<^sub>t n) \<noteq> CHR ''-''
[PROOF STEP]
using Show_nat_not_neg[of \<open>n\<close>]
  Show_nat_not_empty[of \<open>n\<close>] not_hd[of \<open>Show\<^sub>n\<^sub>a\<^sub>t n\<close>]
[PROOF STATE]
proof (prove)
using this:
set (Show\<^sub>n\<^sub>a\<^sub>t n) \<subseteq> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
Show\<^sub>n\<^sub>a\<^sub>t n \<noteq> []
\<lbrakk>Show\<^sub>n\<^sub>a\<^sub>t n \<noteq> []; ?e \<notin> set (Show\<^sub>n\<^sub>a\<^sub>t n)\<rbrakk> \<Longrightarrow> hd (Show\<^sub>n\<^sub>a\<^sub>t n) \<noteq> ?e

goal (1 subgoal):
 1. hd (Show\<^sub>n\<^sub>a\<^sub>t n) \<noteq> CHR ''-''
[PROOF STEP]
by auto


[STATEMENT]
lemma Show_Read_nat_id: \<open>STR_is_nat s \<Longrightarrow> (Show\<^sub>n\<^sub>a\<^sub>t (Read\<^sub>n\<^sub>a\<^sub>t s) = s)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. STR_is_nat s \<Longrightarrow> Show\<^sub>n\<^sub>a\<^sub>t (Read\<^sub>n\<^sub>a\<^sub>t s) = s
[PROOF STEP]
by(simp add:STR_is_nat_def)


[STATEMENT]
lemma bar': \<open>\<forall> d \<in> set l . d < 10 \<Longrightarrow> map nat_of_digit (map digit_of_nat l) = l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>d\<in>set l. d < 10 \<Longrightarrow> map nat_of_digit (map digit_of_nat l) = l
[PROOF STEP]
using  nat_of_digit_digit_of_nat_id
[PROOF STATE]
proof (prove)
using this:
?x < 10 \<Longrightarrow> nat_of_digit (digit_of_nat ?x) = ?x

goal (1 subgoal):
 1. \<forall>d\<in>set l. d < 10 \<Longrightarrow> map nat_of_digit (map digit_of_nat l) = l
[PROOF STEP]
by (simp add: map_idI)


[STATEMENT]
lemma Read_Show_nat_id: \<open>Read\<^sub>n\<^sub>a\<^sub>t(Show\<^sub>n\<^sub>a\<^sub>t n) = n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Read\<^sub>n\<^sub>a\<^sub>t (Show\<^sub>n\<^sub>a\<^sub>t n) = n
[PROOF STEP]
apply(unfold Read\<^sub>n\<^sub>a\<^sub>t_def Show\<^sub>n\<^sub>a\<^sub>t_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_implode (map nat_of_digit (map digit_of_nat (nat_explode n))) = n
[PROOF STEP]
using bar' nat_of_digit_digit_of_nat_id nat_explode_digits
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>set ?l. d < 10 \<Longrightarrow> map nat_of_digit (map digit_of_nat ?l) = ?l
?x < 10 \<Longrightarrow> nat_of_digit (digit_of_nat ?x) = ?x
\<forall>d\<in>set (nat_explode ?n). d < 10

goal (1 subgoal):
 1. nat_implode (map nat_of_digit (map digit_of_nat (nat_explode n))) = n
[PROOF STEP]
using nat_implode_explode_id
[PROOF STATE]
proof (prove)
using this:
\<forall>d\<in>set ?l. d < 10 \<Longrightarrow> map nat_of_digit (map digit_of_nat ?l) = ?l
?x < 10 \<Longrightarrow> nat_of_digit (digit_of_nat ?x) = ?x
\<forall>d\<in>set (nat_explode ?n). d < 10
nat_implode (nat_explode ?n) = ?n

goal (1 subgoal):
 1. nat_implode (map nat_of_digit (map digit_of_nat (nat_explode n))) = n
[PROOF STEP]
by presburger


[STATEMENT]
lemma Show_Read_nat'_id: \<open>strL_is_nat' s \<Longrightarrow> (ShowL\<^sub>n\<^sub>a\<^sub>t (ReadL\<^sub>n\<^sub>a\<^sub>t s) = s)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strL_is_nat' s \<Longrightarrow> \<lfloor>\<lceil>s\<rceil>\<rfloor> = s
[PROOF STEP]
by(simp add:strL_is_nat'_def)


[STATEMENT]
lemma digits_are_ascii:
  \<open>c \<in> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'',
        CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
   \<Longrightarrow> String.ascii_of c = c\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<in> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''} \<Longrightarrow> String.ascii_of c = c
[PROOF STEP]
by auto


[STATEMENT]
lemma Show\<^sub>n\<^sub>a\<^sub>t_ascii: \<open>map String.ascii_of (Show\<^sub>n\<^sub>a\<^sub>t n) = Show\<^sub>n\<^sub>a\<^sub>t n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map String.ascii_of (Show\<^sub>n\<^sub>a\<^sub>t n) = Show\<^sub>n\<^sub>a\<^sub>t n
[PROOF STEP]
using Show_nat_not_neg digits_are_ascii
[PROOF STATE]
proof (prove)
using this:
set (Show\<^sub>n\<^sub>a\<^sub>t ?n) \<subseteq> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''}
?c \<in> {CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9''} \<Longrightarrow> String.ascii_of ?c = ?c

goal (1 subgoal):
 1. map String.ascii_of (Show\<^sub>n\<^sub>a\<^sub>t n) = Show\<^sub>n\<^sub>a\<^sub>t n
[PROOF STEP]
by (meson map_idI subsetD)


[STATEMENT]
lemma Read_Show_nat'_id: \<open>ReadL\<^sub>n\<^sub>a\<^sub>t(ShowL\<^sub>n\<^sub>a\<^sub>t n) = n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>\<lfloor>n\<rfloor>\<rceil> = n
[PROOF STEP]
apply(unfold ReadL\<^sub>n\<^sub>a\<^sub>t_def ShowL\<^sub>n\<^sub>a\<^sub>t_def, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Read\<^sub>n\<^sub>a\<^sub>t (map String.ascii_of (Show\<^sub>n\<^sub>a\<^sub>t n)) = n
[PROOF STEP]
by (simp add: Show\<^sub>n\<^sub>a\<^sub>t_ascii  Read_Show_nat_id)


[STATEMENT]
lemma Show_Read_id: \<open>STR_is_int s \<Longrightarrow> (Show\<^sub>i\<^sub>n\<^sub>t (Read\<^sub>i\<^sub>n\<^sub>t s) = s)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. STR_is_int s \<Longrightarrow> Show\<^sub>i\<^sub>n\<^sub>t (Read\<^sub>i\<^sub>n\<^sub>t s) = s
[PROOF STEP]
by(simp add:STR_is_int_def)


[STATEMENT]
lemma Read_Show_id: \<open>Read\<^sub>i\<^sub>n\<^sub>t(Show\<^sub>i\<^sub>n\<^sub>t(x)) = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Read\<^sub>i\<^sub>n\<^sub>t (Show\<^sub>i\<^sub>n\<^sub>t x) = x
[PROOF STEP]
apply(code_simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if hd (if x < 0 then CHR ''-'' # Show\<^sub>n\<^sub>a\<^sub>t (nat (- x)) else Show\<^sub>n\<^sub>a\<^sub>t (nat x)) = CHR ''-'' then - int (Read\<^sub>n\<^sub>a\<^sub>t (tl (if x < 0 then CHR ''-'' # Show\<^sub>n\<^sub>a\<^sub>t (nat (- x)) else Show\<^sub>n\<^sub>a\<^sub>t (nat x)))) else int (Read\<^sub>n\<^sub>a\<^sub>t (if x < 0 then CHR ''-'' # Show\<^sub>n\<^sub>a\<^sub>t (nat (- x)) else Show\<^sub>n\<^sub>a\<^sub>t (nat x)))) = x
[PROOF STEP]
apply(auto simp:Show_nat_not_neg Read_Show_nat_id)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> x < 0; hd (Show\<^sub>n\<^sub>a\<^sub>t (nat x)) = CHR ''-''\<rbrakk> \<Longrightarrow> - int (Read\<^sub>n\<^sub>a\<^sub>t (tl (Show\<^sub>n\<^sub>a\<^sub>t (nat x)))) = x
[PROOF STEP]
apply(thin_tac \<open>\<not> x < 0 \<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (Show\<^sub>n\<^sub>a\<^sub>t (nat x)) = CHR ''-'' \<Longrightarrow> - int (Read\<^sub>n\<^sub>a\<^sub>t (tl (Show\<^sub>n\<^sub>a\<^sub>t (nat x)))) = x
[PROOF STEP]
using Show_nat_not_neg''
[PROOF STATE]
proof (prove)
using this:
hd (Show\<^sub>n\<^sub>a\<^sub>t ?n) \<noteq> CHR ''-''

goal (1 subgoal):
 1. hd (Show\<^sub>n\<^sub>a\<^sub>t (nat x)) = CHR ''-'' \<Longrightarrow> - int (Read\<^sub>n\<^sub>a\<^sub>t (tl (Show\<^sub>n\<^sub>a\<^sub>t (nat x)))) = x
[PROOF STEP]
by blast


[STATEMENT]
lemma STR_is_int_Show: \<open>STR_is_int (Show\<^sub>i\<^sub>n\<^sub>t n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. STR_is_int (Show\<^sub>i\<^sub>n\<^sub>t n)
[PROOF STEP]
by(simp add:STR_is_int_def Read_Show_id)


[STATEMENT]
lemma Show_ReadL_id: \<open>strL_is_int' s \<Longrightarrow> (ShowL\<^sub>i\<^sub>n\<^sub>t (ReadL\<^sub>i\<^sub>n\<^sub>t s) = s)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strL_is_int' s \<Longrightarrow> \<lfloor>\<lceil>s\<rceil>\<rfloor> = s
[PROOF STEP]
by(simp add:strL_is_int'_def)


[STATEMENT]
lemma Read_ShowL_id: \<open>ReadL\<^sub>i\<^sub>n\<^sub>t (ShowL\<^sub>i\<^sub>n\<^sub>t x) = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
proof(cases \<open>x < 0\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < 0 \<Longrightarrow> \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
 2. \<not> x < 0 \<Longrightarrow> \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < 0

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
 2. \<not> x < 0 \<Longrightarrow> \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < 0

goal (1 subgoal):
 1. \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
using ShowL\<^sub>i\<^sub>n\<^sub>t_def ReadL\<^sub>i\<^sub>n\<^sub>t_def Show\<^sub>i\<^sub>n\<^sub>t_def Show\<^sub>n\<^sub>a\<^sub>t_ascii
[PROOF STATE]
proof (prove)
using this:
x < 0
ShowL\<^sub>i\<^sub>n\<^sub>t = String.implode \<circ> Show\<^sub>i\<^sub>n\<^sub>t
ReadL\<^sub>i\<^sub>n\<^sub>t = Read\<^sub>i\<^sub>n\<^sub>t \<circ> literal.explode
Show\<^sub>i\<^sub>n\<^sub>t ?i = (if ?i < 0 then CHR ''-'' # Show\<^sub>n\<^sub>a\<^sub>t (nat (- ?i)) else Show\<^sub>n\<^sub>a\<^sub>t (nat ?i))
map String.ascii_of (Show\<^sub>n\<^sub>a\<^sub>t ?n) = Show\<^sub>n\<^sub>a\<^sub>t ?n

goal (1 subgoal):
 1. \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
by (metis (no_types, lifting) Read_Show_id String.ascii_of_Char comp_def implode.rep_eq list.simps(9))
[PROOF STATE]
proof (state)
this:
\<lceil>\<lfloor>x\<rfloor>\<rceil> = x

goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < 0

goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> x < 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> x < 0

goal (1 subgoal):
 1. \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
using ShowL\<^sub>i\<^sub>n\<^sub>t_def ReadL\<^sub>i\<^sub>n\<^sub>t_def Show\<^sub>i\<^sub>n\<^sub>t_def Show\<^sub>n\<^sub>a\<^sub>t_ascii
[PROOF STATE]
proof (prove)
using this:
\<not> x < 0
ShowL\<^sub>i\<^sub>n\<^sub>t = String.implode \<circ> Show\<^sub>i\<^sub>n\<^sub>t
ReadL\<^sub>i\<^sub>n\<^sub>t = Read\<^sub>i\<^sub>n\<^sub>t \<circ> literal.explode
Show\<^sub>i\<^sub>n\<^sub>t ?i = (if ?i < 0 then CHR ''-'' # Show\<^sub>n\<^sub>a\<^sub>t (nat (- ?i)) else Show\<^sub>n\<^sub>a\<^sub>t (nat ?i))
map String.ascii_of (Show\<^sub>n\<^sub>a\<^sub>t ?n) = Show\<^sub>n\<^sub>a\<^sub>t ?n

goal (1 subgoal):
 1. \<lceil>\<lfloor>x\<rfloor>\<rceil> = x
[PROOF STEP]
by (metis Read_Show_id String.explode_implode_eq comp_apply)
[PROOF STATE]
proof (state)
this:
\<lceil>\<lfloor>x\<rfloor>\<rceil> = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma STR_is_int_ShowL: \<open>strL_is_int' (ShowL\<^sub>i\<^sub>n\<^sub>t n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strL_is_int' \<lfloor>n\<rfloor>
[PROOF STEP]
by(simp add:strL_is_int'_def Read_ShowL_id)


[STATEMENT]
lemma String_Cancel: "a + (c::String.literal) = b + c \<Longrightarrow> a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + c = b + c \<Longrightarrow> a = b
[PROOF STEP]
using String.plus_literal.rep_eq
[PROOF STATE]
proof (prove)
using this:
literal.explode (?x + ?xa) = literal.explode ?x @ literal.explode ?xa

goal (1 subgoal):
 1. a + c = b + c \<Longrightarrow> a = b
[PROOF STEP]
by (metis append_same_eq literal.explode_inject)


[STATEMENT]
lemma correct:
    shows "policy_axioms sp_spec_subj_obj sp_spec_subj_subj ifp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. policy_axioms sp_spec_subj_obj sp_spec_subj_subj ifp
[PROOF STEP]
proof (unfold_locales)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<forall>p1 p2 f m1 m2. sp_spec_subj_obj p1 (FILEP f) m1 \<and> sp_spec_subj_obj p2 (FILEP f) m2 \<longrightarrow> sp_spec_subj_subj p1 p2
 2. \<forall>p x. sp_spec_subj_obj p (PAGE x) WRITE \<longrightarrow> sp_spec_subj_obj p (PAGE x) READ
 3. \<forall>p. ifp p p
 4. \<forall>a b. sp_spec_subj_subj a b \<longrightarrow> ifp a b \<and> ifp b a
 5. \<forall>a b c x. sp_spec_subj_subj a b \<and> sp_spec_subj_obj b (PAGE x) WRITE \<and> sp_spec_subj_obj c (PAGE x) READ \<longrightarrow> ifp a c
[PROOF STEP]
show sp_spec_file_provider:
      "\<forall> p1 p2 f m1 m2 .
           sp_spec_subj_obj p1 (FILEP f) m1 \<and>
           sp_spec_subj_obj p2 (FILEP f) m2 \<longrightarrow> sp_spec_subj_subj p1 p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p1 p2 f m1 m2. sp_spec_subj_obj p1 (FILEP f) m1 \<and> sp_spec_subj_obj p2 (FILEP f) m2 \<longrightarrow> sp_spec_subj_subj p1 p2
[PROOF STEP]
unfolding sp_spec_subj_subj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p1 p2 f m1 m2. sp_spec_subj_obj p1 (FILEP f) m1 \<and> sp_spec_subj_obj p2 (FILEP f) m2 \<longrightarrow> (\<exists>f m1 m2. sp_spec_subj_obj p1 (FILEP f) m1 \<and> sp_spec_subj_obj p2 (FILEP f) m2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p1 p2 f m1 m2. sp_spec_subj_obj p1 (FILEP f) m1 \<and> sp_spec_subj_obj p2 (FILEP f) m2 \<longrightarrow> sp_spec_subj_subj p1 p2

goal (4 subgoals):
 1. \<forall>p x. sp_spec_subj_obj p (PAGE x) WRITE \<longrightarrow> sp_spec_subj_obj p (PAGE x) READ
 2. \<forall>p. ifp p p
 3. \<forall>a b. sp_spec_subj_subj a b \<longrightarrow> ifp a b \<and> ifp b a
 4. \<forall>a b c x. sp_spec_subj_subj a b \<and> sp_spec_subj_obj b (PAGE x) WRITE \<and> sp_spec_subj_obj c (PAGE x) READ \<longrightarrow> ifp a c
[PROOF STEP]
show sp_spec_no_wronly_pages:
      "\<forall> p x . sp_spec_subj_obj p (PAGE x) WRITE \<longrightarrow> sp_spec_subj_obj p (PAGE x) READ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p x. sp_spec_subj_obj p (PAGE x) WRITE \<longrightarrow> sp_spec_subj_obj p (PAGE x) READ
[PROOF STEP]
unfolding sp_spec_subj_obj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p x. configuration_subj_obj p (PAGE x) WRITE \<or> (\<exists>y. PAGE x = PAGE y \<and> WRITE = READ \<and> configuration_subj_obj p (PAGE x) WRITE) \<longrightarrow> configuration_subj_obj p (PAGE x) READ \<or> (\<exists>y. PAGE x = PAGE y \<and> READ = READ \<and> configuration_subj_obj p (PAGE x) WRITE)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p x. sp_spec_subj_obj p (PAGE x) WRITE \<longrightarrow> sp_spec_subj_obj p (PAGE x) READ

goal (3 subgoals):
 1. \<forall>p. ifp p p
 2. \<forall>a b. sp_spec_subj_subj a b \<longrightarrow> ifp a b \<and> ifp b a
 3. \<forall>a b c x. sp_spec_subj_subj a b \<and> sp_spec_subj_obj b (PAGE x) WRITE \<and> sp_spec_subj_obj c (PAGE x) READ \<longrightarrow> ifp a c
[PROOF STEP]
show ifp_reflexive:
      "\<forall> p . ifp p p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. ifp p p
[PROOF STEP]
unfolding ifp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. sp_spec_subj_subj p p \<or> sp_spec_subj_subj p p \<or> (\<exists>c y. sp_spec_subj_subj p c \<and> sp_spec_subj_obj c (PAGE y) WRITE \<and> sp_spec_subj_obj p (PAGE y) READ) \<or> p = p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p. ifp p p

goal (2 subgoals):
 1. \<forall>a b. sp_spec_subj_subj a b \<longrightarrow> ifp a b \<and> ifp b a
 2. \<forall>a b c x. sp_spec_subj_subj a b \<and> sp_spec_subj_obj b (PAGE x) WRITE \<and> sp_spec_subj_obj c (PAGE x) READ \<longrightarrow> ifp a c
[PROOF STEP]
show ifp_compatible_with_sp_spec:
      "\<forall> a b . sp_spec_subj_subj a b \<longrightarrow> ifp a b \<and> ifp b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. sp_spec_subj_subj a b \<longrightarrow> ifp a b \<and> ifp b a
[PROOF STEP]
unfolding ifp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. sp_spec_subj_subj a b \<longrightarrow> (sp_spec_subj_subj a b \<or> sp_spec_subj_subj b a \<or> (\<exists>c y. sp_spec_subj_subj a c \<and> sp_spec_subj_obj c (PAGE y) WRITE \<and> sp_spec_subj_obj b (PAGE y) READ) \<or> a = b) \<and> (sp_spec_subj_subj b a \<or> sp_spec_subj_subj a b \<or> (\<exists>c y. sp_spec_subj_subj b c \<and> sp_spec_subj_obj c (PAGE y) WRITE \<and> sp_spec_subj_obj a (PAGE y) READ) \<or> b = a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a b. sp_spec_subj_subj a b \<longrightarrow> ifp a b \<and> ifp b a

goal (1 subgoal):
 1. \<forall>a b c x. sp_spec_subj_subj a b \<and> sp_spec_subj_obj b (PAGE x) WRITE \<and> sp_spec_subj_obj c (PAGE x) READ \<longrightarrow> ifp a c
[PROOF STEP]
show ifp_compatible_with_ipc:
      "\<forall> a b c x . (sp_spec_subj_subj a b
                  \<and> sp_spec_subj_obj b (PAGE x) WRITE  \<and> sp_spec_subj_obj c (PAGE x) READ)
                 \<longrightarrow> ifp a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b c x. sp_spec_subj_subj a b \<and> sp_spec_subj_obj b (PAGE x) WRITE \<and> sp_spec_subj_obj c (PAGE x) READ \<longrightarrow> ifp a c
[PROOF STEP]
unfolding ifp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b c x. sp_spec_subj_subj a b \<and> sp_spec_subj_obj b (PAGE x) WRITE \<and> sp_spec_subj_obj c (PAGE x) READ \<longrightarrow> sp_spec_subj_subj a c \<or> sp_spec_subj_subj c a \<or> (\<exists>ca y. sp_spec_subj_subj a ca \<and> sp_spec_subj_obj ca (PAGE y) WRITE \<and> sp_spec_subj_obj c (PAGE y) READ) \<or> a = c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a b c x. sp_spec_subj_subj a b \<and> sp_spec_subj_obj b (PAGE x) WRITE \<and> sp_spec_subj_obj c (PAGE x) READ \<longrightarrow> ifp a c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma example_how_to_use_properties_in_proofs:
  shows "\<forall> p . Policy.ifp p p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. Policy.ifp p p
[PROOF STEP]
using Policy_properties.ifp_reflexive
[PROOF STATE]
proof (prove)
using this:
\<forall>p. Policy.ifp p p

goal (1 subgoal):
 1. \<forall>p. Policy.ifp p p
[PROOF STEP]
by auto


[STATEMENT]
lemma ball_differentiable_atD: "\<forall>x\<in>S. f differentiable at x \<Longrightarrow> f differentiable_on S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S. f differentiable at x \<Longrightarrow> f differentiable_on S
[PROOF STEP]
by (auto simp: differentiable_on_def differentiable_at_withinI)


[STATEMENT]
lemma higher_differentiable_on_imp_continuous_on:
  "continuous_on S f" if "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on S f
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. continuous_on S f
[PROOF STEP]
by (cases n) (auto simp: differentiable_imp_continuous_on ball_differentiable_atD)


[STATEMENT]
lemma higher_differentiable_on_imp_differentiable_on:
  "f differentiable_on S" if "higher_differentiable_on S f k" "k > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f differentiable_on S
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f k
0 < k

goal (1 subgoal):
 1. f differentiable_on S
[PROOF STEP]
by (cases k) (auto simp: ball_differentiable_atD)


[STATEMENT]
lemma higher_differentiable_on_congI:
  assumes "open S" "higher_differentiable_on S g n"
    and "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
  shows "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using assms(2,3)
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S g n
?x \<in> S \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
proof (induction n arbitrary: f g)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on S g 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f 0
 2. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S g n; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f n; higher_differentiable_on S g (Suc n); \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S g 0
?x \<in> S \<Longrightarrow> f ?x = g ?x

goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on S g 0; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f 0
 2. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S g n; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f n; higher_differentiable_on S g (Suc n); \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S g 0
?x \<in> S \<Longrightarrow> f ?x = g ?x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S g 0
?x \<in> S \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. higher_differentiable_on S f 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S g n; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f n; higher_differentiable_on S g (Suc n); \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S g n; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f n; higher_differentiable_on S g (Suc n); \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>higher_differentiable_on S ?g n; \<And>x. x \<in> S \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S ?f n
higher_differentiable_on S g (Suc n)
?x \<in> S \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S g n; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f n; higher_differentiable_on S g (Suc n); \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
have 1: "\<forall>x\<in>S. g differentiable (at x)" and
       2: "higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) v) n" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S. g differentiable at x &&& higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) v) n
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on S ?g n; \<And>x. x \<in> S \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S ?f n
higher_differentiable_on S g (Suc n)
?x \<in> S \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. \<forall>x\<in>S. g differentiable at x &&& higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) v) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. g differentiable at x
higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) ?v) n

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S g n; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f n; higher_differentiable_on S g (Suc n); \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
have 3: "\<forall>x\<in>S. f differentiable (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S. f differentiable at x
[PROOF STEP]
using 1 Suc(3) assms(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. g differentiable at x
?x \<in> S \<Longrightarrow> f ?x = g ?x
open S

goal (1 subgoal):
 1. \<forall>x\<in>S. f differentiable at x
[PROOF STEP]
by (metis differentiable_eqI)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>S. f differentiable at x

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S g n; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f n; higher_differentiable_on S g (Suc n); \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
have 4: "frechet_derivative f (at x) v = frechet_derivative g (at x) v" if "x \<in> S" for x v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frechet_derivative f (at x) v = frechet_derivative g (at x) v
[PROOF STEP]
using "3" Suc.prems(2) assms(1) frechet_derivative_transform_within_open_ext that
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. f differentiable at x
?x \<in> S \<Longrightarrow> f ?x = g ?x
open S
\<lbrakk>?f differentiable at ?xa; open ?X; ?xa \<in> ?X; \<And>x. x \<in> ?X \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> frechet_derivative ?f (at ?xa) ?x = frechet_derivative ?g (at ?xa) ?x
x \<in> S

goal (1 subgoal):
 1. frechet_derivative f (at x) v = frechet_derivative g (at x) v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> frechet_derivative f (at ?x) ?v = frechet_derivative g (at ?x) ?v

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S g n; \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f n; higher_differentiable_on S g (Suc n); \<And>x. x \<in> S \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
from 2 3 4
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) ?v) n
\<forall>x\<in>S. f differentiable at x
?x \<in> S \<Longrightarrow> frechet_derivative f (at ?x) ?v = frechet_derivative g (at ?x) ?v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) ?v) n
\<forall>x\<in>S. f differentiable at x
?x \<in> S \<Longrightarrow> frechet_derivative f (at ?x) ?v = frechet_derivative g (at ?x) ?v

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n)
[PROOF STEP]
using Suc.IH[OF 2 4]
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) ?v) n
\<forall>x\<in>S. f differentiable at x
?x \<in> S \<Longrightarrow> frechet_derivative f (at ?x) ?v = frechet_derivative g (at ?x) ?v
(\<And>x. x \<in> S \<Longrightarrow> x \<in> S) \<Longrightarrow> higher_differentiable_on S (\<lambda>a. frechet_derivative f (at a) ?v3) n

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_on_cong:
  assumes "open S" "S = T"
    and "\<And>x. x \<in> T \<Longrightarrow> f x = g x"
  shows "higher_differentiable_on S f n \<longleftrightarrow> higher_differentiable_on T g n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n = higher_differentiable_on T g n
[PROOF STEP]
using higher_differentiable_on_congI assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>open ?S; higher_differentiable_on ?S ?g ?n; \<And>x. x \<in> ?S \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> higher_differentiable_on ?S ?f ?n
open S
S = T
?x \<in> T \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. higher_differentiable_on S f n = higher_differentiable_on T g n
[PROOF STEP]
by auto


[STATEMENT]
lemma higher_differentiable_on_SucD:
  "higher_differentiable_on S f n" if "higher_differentiable_on S f (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (Suc n)

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by (induction n arbitrary: f) (auto simp: differentiable_imp_continuous_on ball_differentiable_atD)


[STATEMENT]
lemma higher_differentiable_on_addD:
  "higher_differentiable_on S f n" if "higher_differentiable_on S f (n + m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (n + m)

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by (induction m arbitrary: f n)
    (auto simp del: higher_differentiable_on.simps dest!: higher_differentiable_on_SucD)


[STATEMENT]
lemma higher_differentiable_on_le:
  "higher_differentiable_on S f n" if "higher_differentiable_on S f m" "n \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using higher_differentiable_on_addD[of S f n "m - n"] that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (n + (m - n)) \<Longrightarrow> higher_differentiable_on S f n
higher_differentiable_on S f m
n \<le> m

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by auto


[STATEMENT]
lemma higher_differentiable_on_open_subsetsI:
  "higher_differentiable_on S f n"
  if "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> \<exists>T. ?x \<in> T \<and> open T \<and> higher_differentiable_on T f n

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
proof (induction n arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f 0) \<Longrightarrow> higher_differentiable_on S f 0
 2. \<And>n f. \<lbrakk>\<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f n) \<Longrightarrow> higher_differentiable_on S f n; \<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> \<exists>T. ?x \<in> T \<and> open T \<and> higher_differentiable_on T f 0

goal (2 subgoals):
 1. \<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f 0) \<Longrightarrow> higher_differentiable_on S f 0
 2. \<And>n f. \<lbrakk>\<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f n) \<Longrightarrow> higher_differentiable_on S f n; \<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f 0
[PROOF STEP]
by (force simp: continuous_on_def
        dest!: 0
        dest: at_within_open
        intro!: Lim_at_imp_Lim_at_within[where S=S])
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f n) \<Longrightarrow> higher_differentiable_on S f n; \<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f n) \<Longrightarrow> higher_differentiable_on S f n; \<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T ?f n) \<Longrightarrow> higher_differentiable_on S ?f n
?x \<in> S \<Longrightarrow> \<exists>T. ?x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f n) \<Longrightarrow> higher_differentiable_on S f n; \<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
have "f differentiable at x" if "x \<in> S" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f differentiable at x
[PROOF STEP]
using Suc.prems[OF \<open>x \<in> S\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)

goal (1 subgoal):
 1. f differentiable at x
[PROOF STEP]
by (auto simp: differentiable_on_def dest: at_within_open dest!: bspec)
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> f differentiable at ?x

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f n) \<Longrightarrow> higher_differentiable_on S f n; \<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> S \<Longrightarrow> f differentiable at ?x
[PROOF STEP]
have "f differentiable_on S"
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> f differentiable at ?x

goal (1 subgoal):
 1. f differentiable_on S
[PROOF STEP]
by (auto simp: differentiable_on_def intro!: differentiable_at_withinI[where s=S])
[PROOF STATE]
proof (state)
this:
f differentiable_on S

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. (\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f n) \<Longrightarrow> higher_differentiable_on S f n; \<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)\<rbrakk> \<Longrightarrow> higher_differentiable_on S f (Suc n)
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
(\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T ?f n) \<Longrightarrow> higher_differentiable_on S ?f n
?x \<in> S \<Longrightarrow> \<exists>T. ?x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)
f differentiable_on S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> S \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> higher_differentiable_on T ?f n) \<Longrightarrow> higher_differentiable_on S ?f n
?x \<in> S \<Longrightarrow> \<exists>T. ?x \<in> T \<and> open T \<and> higher_differentiable_on T f (Suc n)
f differentiable_on S

goal (1 subgoal):
 1. higher_differentiable_on S f (Suc n)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_on_const: "higher_differentiable_on S (\<lambda>x. c) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. c) n
[PROOF STEP]
by (induction n arbitrary: c) (auto simp: continuous_intros frechet_derivative_const)


[STATEMENT]
lemma higher_differentiable_on_id: "higher_differentiable_on S (\<lambda>x. x) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. x) n
[PROOF STEP]
by (cases n) (auto simp: frechet_derivative_works higher_differentiable_on_const)


[STATEMENT]
lemma higher_differentiable_on_add:
  "higher_differentiable_on S (\<lambda>x. f x + g x) n"
  if "higher_differentiable_on S f n"
    "higher_differentiable_on S g n"
    "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x + g x) n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n
higher_differentiable_on S g n
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x + g x) n
[PROOF STEP]
proof (induction n arbitrary: f g)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on S f 0; higher_differentiable_on S g 0; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) 0
 2. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0
open S

goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on S f 0; higher_differentiable_on S g 0; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) 0
 2. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x + g x) 0
[PROOF STEP]
by (auto intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. f x + g x) 0

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>higher_differentiable_on S ?f n; higher_differentiable_on S ?g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. ?f x + ?g x) n
higher_differentiable_on S f (Suc n)
higher_differentiable_on S g (Suc n)
open S

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f (Suc n)
higher_differentiable_on S g (Suc n)
open S
[PROOF STEP]
have
    f: "\<And>x. x\<in>S \<Longrightarrow> f differentiable (at x)"
    and hf: "higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n"
    and g: "\<And>x. x\<in>S \<Longrightarrow> g differentiable (at x)"
    and hg: "higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) v) n"
    for v
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (Suc n)
higher_differentiable_on S g (Suc n)
open S

goal (1 subgoal):
 1. ((\<And>x. x \<in> S \<Longrightarrow> f differentiable at x) &&& higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n) &&& (\<And>x. x \<in> S \<Longrightarrow> g differentiable at x) &&& higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) v) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> f differentiable at ?x
higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) ?v) n
?x \<in> S \<Longrightarrow> g differentiable at ?x
higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) ?v) n

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)
[PROOF STEP]
using f g \<open>open S\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> f differentiable at ?x
?x \<in> S \<Longrightarrow> g differentiable at ?x
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)
[PROOF STEP]
by (auto simp: frechet_derivative_plus
        intro!: derivative_intros f g Suc.IH hf hg
        cong: higher_differentiable_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. f x + g x) (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in bounded_bilinear) differentiable:
 "(\<lambda>x. prod (f x) (g x)) differentiable at x within S"
 if "f differentiable at x within S"
    "g differentiable at x within S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x ** g x) differentiable at x within S
[PROOF STEP]
by (blast intro: differentiableI frechet_derivative_worksI that FDERIV)


[STATEMENT]
lemma (in bounded_bilinear) differentiable_on:
  "(\<lambda>x. prod (f x) (g x)) differentiable_on S"
  if "f differentiable_on S" "g differentiable_on S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. f x ** g x) differentiable_on S
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
f differentiable_on S
g differentiable_on S

goal (1 subgoal):
 1. (\<lambda>x. f x ** g x) differentiable_on S
[PROOF STEP]
by (auto simp: differentiable_on_def differentiable)


[STATEMENT]
lemma (in bounded_bilinear) higher_differentiable_on:
  "higher_differentiable_on S (\<lambda>x. prod (f x) (g x)) n"
  if
    "higher_differentiable_on S f n"
    "higher_differentiable_on S g n"
    "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x ** g x) n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n
higher_differentiable_on S g n
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x ** g x) n
[PROOF STEP]
proof (induction n arbitrary: f g)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on S f 0; higher_differentiable_on S g 0; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) 0
 2. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0
open S

goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on S f 0; higher_differentiable_on S g 0; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) 0
 2. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 0
higher_differentiable_on S g 0
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x ** g x) 0
[PROOF STEP]
by (auto intro!: continuous_intros continuous_on)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. f x ** g x) 0

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>higher_differentiable_on S ?f n; higher_differentiable_on S ?g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. ?f x ** ?g x) n
higher_differentiable_on S f (Suc n)
higher_differentiable_on S g (Suc n)
open S

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f (Suc n)
higher_differentiable_on S g (Suc n)
open S
[PROOF STEP]
have
    f: "\<And>x. x\<in>S \<Longrightarrow> f differentiable (at x)"
    and hf: "higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n"
    and g: "\<And>x. x\<in>S \<Longrightarrow> g differentiable (at x)"
    and hg: "higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) v) n"
    for v
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (Suc n)
higher_differentiable_on S g (Suc n)
open S

goal (1 subgoal):
 1. ((\<And>x. x \<in> S \<Longrightarrow> f differentiable at x) &&& higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) v) n) &&& (\<And>x. x \<in> S \<Longrightarrow> g differentiable at x) &&& higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) v) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> S \<Longrightarrow> f differentiable at ?x
higher_differentiable_on S (\<lambda>x. frechet_derivative f (at x) ?v) n
?x \<in> S \<Longrightarrow> g differentiable at ?x
higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) ?v) n

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on S f n; higher_differentiable_on S g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) n; higher_differentiable_on S f (Suc n); higher_differentiable_on S g (Suc n); open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)
[PROOF STEP]
using f g \<open>open S\<close> Suc
[PROOF STATE]
proof (prove)
using this:
?x \<in> S \<Longrightarrow> f differentiable at ?x
?x \<in> S \<Longrightarrow> g differentiable at ?x
open S
\<lbrakk>higher_differentiable_on S ?f n; higher_differentiable_on S ?g n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. ?f x ** ?g x) n
higher_differentiable_on S f (Suc n)
higher_differentiable_on S g (Suc n)
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)
[PROOF STEP]
by (auto simp: frechet_derivative
        intro!: derivative_intros f g differentiable higher_differentiable_on_add Suc.IH
        intro: higher_differentiable_on_SucD
        cong: higher_differentiable_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. f x ** g x) (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_on_sum:
  "higher_differentiable_on S (\<lambda>x. \<Sum>i\<in>F. f i x) n"
  if "\<And>i. i \<in> F \<Longrightarrow> finite F \<Longrightarrow> higher_differentiable_on S (f i) n" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. \<Sum>i\<in>F. f i x) n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i \<in> F; finite F\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f ?i) n
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. \<Sum>i\<in>F. f i x) n
[PROOF STEP]
by (induction F rule: infinite_finite_induct)
    (auto intro!: higher_differentiable_on_const higher_differentiable_on_add)


[STATEMENT]
lemma higher_differentiable_on_subset:
  "higher_differentiable_on S f n"
  if "higher_differentiable_on T f n" "S \<subseteq> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on T f n
S \<subseteq> T

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by (induction n arbitrary: f) (auto intro: continuous_on_subset differentiable_on_subset)


[STATEMENT]
lemma higher_differentiable_on_compose:
  "higher_differentiable_on S (f o g) n"
  if "higher_differentiable_on T f n" "higher_differentiable_on S g n"  "g ` S \<subseteq> T" "open S" "open T"
  for g::"_\<Rightarrow>_::euclidean_space"\<comment>\<open>TODO: can we get around this restriction?\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (f \<circ> g) n
[PROOF STEP]
using that(1-3)
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on T f n
higher_differentiable_on S g n
g ` S \<subseteq> T

goal (1 subgoal):
 1. higher_differentiable_on S (f \<circ> g) n
[PROOF STEP]
proof (induction n arbitrary: f g)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on T f 0; higher_differentiable_on S g 0; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) 0
 2. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on T f n; higher_differentiable_on S g n; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) n; higher_differentiable_on T f (Suc n); higher_differentiable_on S g (Suc n); g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on T f 0
higher_differentiable_on S g 0
g ` S \<subseteq> T

goal (2 subgoals):
 1. \<And>f g. \<lbrakk>higher_differentiable_on T f 0; higher_differentiable_on S g 0; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) 0
 2. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on T f n; higher_differentiable_on S g n; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) n; higher_differentiable_on T f (Suc n); higher_differentiable_on S g (Suc n); g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on T f 0
higher_differentiable_on S g 0
g ` S \<subseteq> T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on T f 0
higher_differentiable_on S g 0
g ` S \<subseteq> T

goal (1 subgoal):
 1. higher_differentiable_on S (f \<circ> g) 0
[PROOF STEP]
using that(4-)
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on T f 0
higher_differentiable_on S g 0
g ` S \<subseteq> T
open S
open T

goal (1 subgoal):
 1. higher_differentiable_on S (f \<circ> g) 0
[PROOF STEP]
by (auto simp: continuous_on_compose2)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (f \<circ> g) 0

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on T f n; higher_differentiable_on S g n; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) n; higher_differentiable_on T f (Suc n); higher_differentiable_on S g (Suc n); g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on T f n; higher_differentiable_on S g n; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) n; higher_differentiable_on T f (Suc n); higher_differentiable_on S g (Suc n); g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>higher_differentiable_on T ?f n; higher_differentiable_on S ?g n; ?g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (?f \<circ> ?g) n
higher_differentiable_on T f (Suc n)
higher_differentiable_on S g (Suc n)
g ` S \<subseteq> T

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on T f n; higher_differentiable_on S g n; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) n; higher_differentiable_on T f (Suc n); higher_differentiable_on S g (Suc n); g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) (Suc n)
[PROOF STEP]
from Suc.prems
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on T f (Suc n)
higher_differentiable_on S g (Suc n)
g ` S \<subseteq> T
[PROOF STEP]
have
    f: "\<And>x. x \<in> T \<Longrightarrow> f differentiable (at x)"
    and g: "\<And>x. x \<in> S \<Longrightarrow> g differentiable (at x)"
    and hf: "higher_differentiable_on T (\<lambda>x. frechet_derivative f (at x) v) n"
    and hg: "higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) w) n"
    for v w
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on T f (Suc n)
higher_differentiable_on S g (Suc n)
g ` S \<subseteq> T

goal (1 subgoal):
 1. ((\<And>x. x \<in> T \<Longrightarrow> f differentiable at x) &&& (\<And>x. x \<in> S \<Longrightarrow> g differentiable at x)) &&& higher_differentiable_on T (\<lambda>x. frechet_derivative f (at x) v) n &&& higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) w) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> T \<Longrightarrow> f differentiable at ?x
?x \<in> S \<Longrightarrow> g differentiable at ?x
higher_differentiable_on T (\<lambda>x. frechet_derivative f (at x) ?v) n
higher_differentiable_on S (\<lambda>x. frechet_derivative g (at x) ?w) n

goal (1 subgoal):
 1. \<And>n f g. \<lbrakk>\<And>f g. \<lbrakk>higher_differentiable_on T f n; higher_differentiable_on S g n; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) n; higher_differentiable_on T f (Suc n); higher_differentiable_on S g (Suc n); g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (f \<circ> g) (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (f \<circ> g) (Suc n)
[PROOF STEP]
using \<open>g ` _ \<subseteq> _\<close> \<open>open S\<close> f g \<open>open T\<close> Suc
      Suc.IH[where f="\<lambda>x. frechet_derivative f (at x) v"
        and g = "\<lambda>x. g x" for v, unfolded o_def]
      higher_differentiable_on_SucD[OF Suc.prems(2)]
[PROOF STATE]
proof (prove)
using this:
g ` S \<subseteq> T
open S
?x \<in> T \<Longrightarrow> f differentiable at ?x
?x \<in> S \<Longrightarrow> g differentiable at ?x
open T
\<lbrakk>higher_differentiable_on T ?f n; higher_differentiable_on S ?g n; ?g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (?f \<circ> ?g) n
higher_differentiable_on T f (Suc n)
higher_differentiable_on S g (Suc n)
g ` S \<subseteq> T
\<lbrakk>higher_differentiable_on T (\<lambda>a. frechet_derivative f (at a) ?v2) n; higher_differentiable_on S g n; g ` S \<subseteq> T\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>a. frechet_derivative f (at (g a)) ?v2) n
higher_differentiable_on S g n

goal (1 subgoal):
 1. higher_differentiable_on S (f \<circ> g) (Suc n)
[PROOF STEP]
by (auto
        simp: frechet_derivative_compose_eucl subset_iff
        simp del: o_apply
        intro!: differentiable_chain_within higher_differentiable_on_sum
          higher_differentiable_on_scaleR higher_differentiable_on_inner
          higher_differentiable_on_const
        intro: differentiable_at_withinI
        cong: higher_differentiable_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (f \<circ> g) (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_on_uminus:
  "higher_differentiable_on S (\<lambda>x. - f x) n"
  if "higher_differentiable_on S f n" "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. - f x) n
[PROOF STEP]
using higher_differentiable_on_scaleR[of S "\<lambda>x. -1" n f] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on S (\<lambda>x. - 1) n; higher_differentiable_on S f n; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. - 1 *\<^sub>R f x) n
higher_differentiable_on S f n
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. - f x) n
[PROOF STEP]
by (auto simp: higher_differentiable_on_const)


[STATEMENT]
lemma higher_differentiable_on_minus:
  "higher_differentiable_on S (\<lambda>x. f x - g x) n"
  if "higher_differentiable_on S f n"
    "higher_differentiable_on S g n"
    "open S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x - g x) n
[PROOF STEP]
using higher_differentiable_on_add[OF _ higher_differentiable_on_uminus, OF that(1,2,3,3)]
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S (\<lambda>x. f x + - g x) n

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x - g x) n
[PROOF STEP]
by simp


[STATEMENT]
lemma higher_differentiable_on_inverse:
  "higher_differentiable_on S (\<lambda>x. inverse (f x)) n"
  if "higher_differentiable_on S f n" "0 \<notin> f ` S" "open S"
  for f::"_\<Rightarrow>_::real_normed_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. inverse (f x)) n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f n
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. inverse (f x)) n
[PROOF STEP]
proof (induction n arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>higher_differentiable_on S f 0; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) 0
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f 0
(0::'d) \<notin> f ` S
open S

goal (2 subgoals):
 1. \<And>f. \<lbrakk>higher_differentiable_on S f 0; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) 0
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f 0
(0::'d) \<notin> f ` S
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f 0
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. inverse (f x)) 0
[PROOF STEP]
by (auto simp: continuous_on_inverse)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. inverse (f x)) 0

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>higher_differentiable_on S ?f n; (0::'d) \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (?f x)) n
higher_differentiable_on S f (Suc n)
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) (Suc n)
[PROOF STEP]
from Suc.prems(1)
[PROOF STATE]
proof (chain)
picking this:
higher_differentiable_on S f (Suc n)
[PROOF STEP]
have fn: "higher_differentiable_on S f n"
[PROOF STATE]
proof (prove)
using this:
higher_differentiable_on S f (Suc n)

goal (1 subgoal):
 1. higher_differentiable_on S f n
[PROOF STEP]
by (rule higher_differentiable_on_SucD)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S f n

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>higher_differentiable_on S f n; (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) n; higher_differentiable_on S f (Suc n); (0::'d) \<notin> f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (f x)) (Suc n)
[PROOF STEP]
from Suc
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>higher_differentiable_on S ?f n; (0::'d) \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (?f x)) n
higher_differentiable_on S f (Suc n)
(0::'d) \<notin> f ` S
open S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>higher_differentiable_on S ?f n; (0::'d) \<notin> ?f ` S; open S\<rbrakk> \<Longrightarrow> higher_differentiable_on S (\<lambda>x. inverse (?f x)) n
higher_differentiable_on S f (Suc n)
(0::'d) \<notin> f ` S
open S

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. inverse (f x)) (Suc n)
[PROOF STEP]
by (auto simp: continuous_on_inverse image_iff power2_eq_square
        frechet_derivative_inverse divide_inverse
        intro!: differentiable_inverse higher_differentiable_on_uminus higher_differentiable_on_mult
          Suc.IH fn
        cong: higher_differentiable_on_cong)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on S (\<lambda>x. inverse (f x)) (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higher_differentiable_on_divide:
  "higher_differentiable_on S (\<lambda>x. f x / g x) n"
  if
    "higher_differentiable_on S f n"
    "higher_differentiable_on S g n"
    "\<And>x. x \<in> S \<Longrightarrow> g x \<noteq> 0"
    "open S"
  for f::"_\<Rightarrow>_::real_normed_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x / g x) n
[PROOF STEP]
using higher_differentiable_on_mult[OF _ higher_differentiable_on_inverse, OF that(1,2) _ that(4,4)]
    that(3)
[PROOF STATE]
proof (prove)
using this:
(0::'d) \<notin> g ` S \<Longrightarrow> higher_differentiable_on S (\<lambda>x. f x * inverse (g x)) n
?x \<in> S \<Longrightarrow> g ?x \<noteq> (0::'d)

goal (1 subgoal):
 1. higher_differentiable_on S (\<lambda>x. f x / g x) n
[PROOF STEP]
by (auto simp: divide_inverse image_iff)


[STATEMENT]
lemma differentiable_on_open_Union:
  "f differentiable_on \<Union>S"
  if "\<And>s. s \<in> S \<Longrightarrow> f differentiable_on s"
    "\<And>s. s \<in> S \<Longrightarrow> open s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f differentiable_on \<Union> S
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> f differentiable_on ?s
?s \<in> S \<Longrightarrow> open ?s

goal (1 subgoal):
 1. f differentiable_on \<Union> S
[PROOF STEP]
unfolding differentiable_on_def
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> \<forall>x\<in>?s. f differentiable at x within ?s
?s \<in> S \<Longrightarrow> open ?s

goal (1 subgoal):
 1. \<forall>x\<in>\<Union> S. f differentiable at x within \<Union> S
[PROOF STEP]
by (metis Union_iff at_within_open open_Union)


[STATEMENT]
lemma higher_differentiable_on_open_Union: "higher_differentiable_on (\<Union>S) f n"
  if "\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f n"
    "\<And>s. s \<in> S \<Longrightarrow> open s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on (\<Union> S) f n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> higher_differentiable_on ?s f n
?s \<in> S \<Longrightarrow> open ?s

goal (1 subgoal):
 1. higher_differentiable_on (\<Union> S) f n
[PROOF STEP]
proof (induction n arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f 0; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f 0
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f n; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f n; \<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f (Suc n); \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
?s \<in> S \<Longrightarrow> higher_differentiable_on ?s f 0
?s \<in> S \<Longrightarrow> open ?s

goal (2 subgoals):
 1. \<And>f. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f 0; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f 0
 2. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f n; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f n; \<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f (Suc n); \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?s \<in> S \<Longrightarrow> higher_differentiable_on ?s f 0
?s \<in> S \<Longrightarrow> open ?s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> higher_differentiable_on ?s f 0
?s \<in> S \<Longrightarrow> open ?s

goal (1 subgoal):
 1. higher_differentiable_on (\<Union> S) f 0
[PROOF STEP]
by (auto simp: continuous_on_open_Union)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (\<Union> S) f 0

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f n; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f n; \<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f (Suc n); \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f n; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f n; \<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f (Suc n); \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s ?f n; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) ?f n
?s \<in> S \<Longrightarrow> higher_differentiable_on ?s f (Suc n)
?s \<in> S \<Longrightarrow> open ?s

goal (1 subgoal):
 1. \<And>n f. \<lbrakk>\<And>f. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f n; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f n; \<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s f (Suc n); \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s ?f n; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) ?f n
?s \<in> S \<Longrightarrow> higher_differentiable_on ?s f (Suc n)
?s \<in> S \<Longrightarrow> open ?s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>s. s \<in> S \<Longrightarrow> higher_differentiable_on s ?f n; \<And>s. s \<in> S \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> S) ?f n
?s \<in> S \<Longrightarrow> higher_differentiable_on ?s f (Suc n)
?s \<in> S \<Longrightarrow> open ?s

goal (1 subgoal):
 1. higher_differentiable_on (\<Union> S) f (Suc n)
[PROOF STEP]
by (auto simp: differentiable_on_open_Union)
[PROOF STATE]
proof (state)
this:
higher_differentiable_on (\<Union> S) f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma differentiable_on_open_Un:
  "f differentiable_on S \<union> T"
  if "f differentiable_on S"
    "f differentiable_on T"
    "open S" "open T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f differentiable_on S \<union> T
[PROOF STEP]
using that differentiable_on_open_Union[of "{S, T}" f]
[PROOF STATE]
proof (prove)
using this:
f differentiable_on S
f differentiable_on T
open S
open T
\<lbrakk>\<And>s. s \<in> {S, T} \<Longrightarrow> f differentiable_on s; \<And>s. s \<in> {S, T} \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> f differentiable_on \<Union> {S, T}

goal (1 subgoal):
 1. f differentiable_on S \<union> T
[PROOF STEP]
by auto


[STATEMENT]
lemma higher_differentiable_on_open_Un: "higher_differentiable_on (S \<union> T) f n"
  if "higher_differentiable_on S f n"
    "higher_differentiable_on T f n"
    "open S" "open T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higher_differentiable_on (S \<union> T) f n
[PROOF STEP]
using higher_differentiable_on_open_Union[of "{S, T}" f n] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>s. s \<in> {S, T} \<Longrightarrow> higher_differentiable_on s f n; \<And>s. s \<in> {S, T} \<Longrightarrow> open s\<rbrakk> \<Longrightarrow> higher_differentiable_on (\<Union> {S, T}) f n
higher_differentiable_on S f n
higher_differentiable_on T f n
open S
open T

goal (1 subgoal):
 1. higher_differentiable_on (S \<union> T) f n
[PROOF STEP]
by auto