[STATEMENT]
lemma Entry_sourcenode_hd:
  assumes "n -as\<rightarrow>* n'" and "(_Entry_) \<in> set (sourcenodes as)"
  shows "n = (_Entry_)" and "(_Entry_) \<notin> set (sourcenodes (tl as))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = (_Entry_) &&& (_Entry_) \<notin> set (sourcenodes (tl as))
[PROOF STEP]
using \<open>n -as\<rightarrow>* n'\<close> \<open>(_Entry_) \<in> set (sourcenodes as)\<close>
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n'
(_Entry_) \<in> set (sourcenodes as)

goal (1 subgoal):
 1. n = (_Entry_) &&& (_Entry_) \<notin> set (sourcenodes (tl as))
[PROOF STEP]
proof(induct rule:path.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl []))
 3. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 4. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
case (empty_path n)
[PROOF STATE]
proof (state)
this:
valid_node n

goal (4 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl []))
 3. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 4. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes [])

goal (4 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl []))
 3. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 4. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(_Entry_) \<in> set (sourcenodes [])

goal (1 subgoal):
 1. n = (_Entry_)
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
n = (_Entry_)

goal (3 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl []))
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 3. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl []))
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 3. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
case (empty_path n)
[PROOF STATE]
proof (state)
this:
valid_node n

goal (3 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl []))
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 3. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes [])

goal (3 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; (_Entry_) \<in> set (sourcenodes [])\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl []))
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 3. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(_Entry_) \<in> set (sourcenodes [])

goal (1 subgoal):
 1. (_Entry_) \<notin> set (sourcenodes (tl []))
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
(_Entry_) \<notin> set (sourcenodes (tl []))

goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
case (Cons_path n'' as n' a n)
[PROOF STATE]
proof (state)
this:
n'' -as\<rightarrow>* n'
(_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_)
(_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as))
valid_edge a
sourcenode a = n
targetnode a = n''

goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
note IH1 = \<open>(_Entry_) \<in> set(sourcenodes as) \<Longrightarrow> n'' = (_Entry_)\<close>
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_)

goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
note IH2 = \<open>(_Entry_) \<in> set(sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set(sourcenodes(tl as))\<close>
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as))

goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
have "(_Entry_) \<notin> set (sourcenodes(tl(a#as)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (_Entry_) \<in> set (sourcenodes (tl (a # as))) \<Longrightarrow> False
[PROOF STEP]
assume "(_Entry_) \<in> set (sourcenodes (tl (a#as)))"
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes (tl (a # as)))

goal (1 subgoal):
 1. (_Entry_) \<in> set (sourcenodes (tl (a # as))) \<Longrightarrow> False
[PROOF STEP]
hence "(_Entry_) \<in> set (sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) \<in> set (sourcenodes (tl (a # as)))

goal (1 subgoal):
 1. (_Entry_) \<in> set (sourcenodes as)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes as)

goal (1 subgoal):
 1. (_Entry_) \<in> set (sourcenodes (tl (a # as))) \<Longrightarrow> False
[PROOF STEP]
from IH1[OF this]
[PROOF STATE]
proof (chain)
picking this:
n'' = (_Entry_)
[PROOF STEP]
have "n'' = (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
n'' = (_Entry_)

goal (1 subgoal):
 1. n'' = (_Entry_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n'' = (_Entry_)

goal (1 subgoal):
 1. (_Entry_) \<in> set (sourcenodes (tl (a # as))) \<Longrightarrow> False
[PROOF STEP]
with \<open>targetnode a = n''\<close> \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a = n''
valid_edge a
n'' = (_Entry_)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
targetnode a = n''
valid_edge a
n'' = (_Entry_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(erule Entry_target,simp)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))

goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
hence "(_Entry_) \<notin> set (sourcenodes(tl(a#as)))"
[PROOF STATE]
proof (prove)
using this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))

goal (1 subgoal):
 1. (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))

goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))

goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes (a # as))

goal (2 subgoals):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> n = (_Entry_)
 2. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
with \<open>(_Entry_) \<notin> set (sourcenodes(tl(a#as)))\<close> \<open>sourcenode a = n\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))
sourcenode a = n
(_Entry_) \<in> set (sourcenodes (a # as))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))
sourcenode a = n
(_Entry_) \<in> set (sourcenodes (a # as))

goal (1 subgoal):
 1. n = (_Entry_)
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
n = (_Entry_)

goal (1 subgoal):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes (a # as))

goal (1 subgoal):
 1. \<And>n'' as n' a n. \<lbrakk>n'' -as\<rightarrow>* n'; (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> n'' = (_Entry_); (_Entry_) \<in> set (sourcenodes as) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl as)); valid_edge a; sourcenode a = n; targetnode a = n''; (_Entry_) \<in> set (sourcenodes (a # as))\<rbrakk> \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
with \<open>(_Entry_) \<notin> set (sourcenodes(tl(a#as)))\<close> \<open>sourcenode a = n\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))
sourcenode a = n
(_Entry_) \<in> set (sourcenodes (a # as))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))
sourcenode a = n
(_Entry_) \<in> set (sourcenodes (a # as))

goal (1 subgoal):
 1. (_Entry_) \<notin> set (sourcenodes (tl (a # as)))
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
(_Entry_) \<notin> set (sourcenodes (tl (a # as)))

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(_Entry_) \<in> set (sourcenodes (a # as)) \<Longrightarrow> (_Entry_) \<notin> set (sourcenodes (tl (a # as)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hypext_Hyperdual_eq:
  "(*h* f) (Hyperdual a b c d) =
     Hyperdual (f a) (b * deriv f a) (c * deriv f a) (d * deriv f a + b * c * deriv (deriv f) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* f) (Hyperdual a b c d) = Hyperdual (f a) (b * deriv f a) (c * deriv f a) (d * deriv f a + b * c * deriv (deriv f) a)
[PROOF STEP]
by (simp add: hypext.code)


[STATEMENT]
lemma hypext_Hyperdual_eq_parts:
  "(*h* f) (Hyperdual a b c d) =
      f a *\<^sub>H ba + (b * deriv f a) *\<^sub>H e1 + (c * deriv f a) *\<^sub>H e2 +
         (d * deriv f a + b * c * deriv (deriv f) a) *\<^sub>H e12 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* f) (Hyperdual a b c d) = f a *\<^sub>H ba + (b * deriv f a) *\<^sub>H e1 + (c * deriv f a) *\<^sub>H e2 + (d * deriv f a + b * c * deriv (deriv f) a) *\<^sub>H e12
[PROOF STEP]
by (metis Hyperdual_eq hypext_Hyperdual_eq)


[STATEMENT]
lemma hyperdualx_sel [simp]:
  shows "Base (\<beta> x) = x"
    and "Eps1 (\<beta> x) = 1"
    and "Eps2 (\<beta> x) = 1"
    and "Eps12 (\<beta> x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Base (\<beta> x) = x &&& Eps1 (\<beta> x) = (1::'a)) &&& Eps2 (\<beta> x) = (1::'a) &&& Eps12 (\<beta> x) = (0::'a)
[PROOF STEP]
by (simp_all add: hyperdualx_def)


[STATEMENT]
lemma hypext_extract_eq:
  "(*h* f) (\<beta> x) = f x *\<^sub>H ba + deriv f x *\<^sub>H e1 + deriv f x *\<^sub>H e2 + deriv (deriv f) x *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* f) (\<beta> x) = f x *\<^sub>H ba + deriv f x *\<^sub>H e1 + deriv f x *\<^sub>H e2 + deriv (deriv f) x *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_Hyperdual_eq_parts hyperdualx_def)


[STATEMENT]
lemma Base_hypext:
  "Base ((*h* f) (\<beta> x)) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Base ((*h* f) (\<beta> x)) = f x
[PROOF STEP]
by (simp add: hyperdualx_def)


[STATEMENT]
lemma Eps1_hypext:
  "Eps1 ((*h* f) (\<beta> x)) = deriv f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps1 ((*h* f) (\<beta> x)) = deriv f x
[PROOF STEP]
by (simp add: hyperdualx_def)


[STATEMENT]
lemma Eps2_hypext:
  "Eps2 ((*h* f) (\<beta> x)) = deriv f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps2 ((*h* f) (\<beta> x)) = deriv f x
[PROOF STEP]
by (simp add: hyperdualx_def)


[STATEMENT]
lemma Eps12_hypext:
  "Eps12 ((*h* f) (\<beta> x)) = deriv (deriv f) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 ((*h* f) (\<beta> x)) = deriv (deriv f) x
[PROOF STEP]
by (simp add: hyperdualx_def)


[STATEMENT]
lemma autodiff_sel:
  "Value (autodiff f x) = Base ((*h* f) (\<beta> x))"
  "First (autodiff f x) = Eps1 ((*h* f) (\<beta> x))"
  "Second (autodiff f x) = Eps12 ((*h* f) (\<beta> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Value (autodiff f x) = Base ((*h* f) (\<beta> x)) &&& First (autodiff f x) = Eps1 ((*h* f) (\<beta> x)) &&& Second (autodiff f x) = Eps12 ((*h* f) (\<beta> x))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma autodiff_extract_value:
  "Value (autodiff f x) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Value (autodiff f x) = f x
[PROOF STEP]
by (simp del: hypext.simps add: Base_hypext)


[STATEMENT]
lemma autodiff_extract_first:
  "First (autodiff f x) = deriv f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. First (autodiff f x) = deriv f x
[PROOF STEP]
by (simp del: hypext.simps add: Eps1_hypext)


[STATEMENT]
lemma autodiff_extract_second:
  "Second (autodiff f x) = deriv (deriv f) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Second (autodiff f x) = deriv (deriv f) x
[PROOF STEP]
by (simp del: hypext.simps add: Eps12_hypext)


[STATEMENT]
lemma autodiff_first_derivative:
  assumes "f field_differentiable (at x)"
  shows "(f has_field_derivative First (autodiff f x)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f has_field_derivative First (autodiff f x)) (at x)
[PROOF STEP]
by (simp add: autodiff_extract_first DERIV_deriv_iff_field_differentiable assms)


[STATEMENT]
lemma autodiff_second_derivative:
  assumes "f twice_field_differentiable_at x"
  shows "((deriv f) has_field_derivative Second (autodiff f x)) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (deriv f has_field_derivative Second (autodiff f x)) (at x)
[PROOF STEP]
by (simp add: autodiff_extract_second DERIV_deriv_iff_field_differentiable assms deriv_field_differentiable_at)


[STATEMENT]
lemma hypext_compose:
  assumes "f twice_field_differentiable_at (Base x)"
      and "g twice_field_differentiable_at (f (Base x))"
    shows "(*h* (\<lambda>x. g (f x))) x = (*h* g) ((*h* f) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. g (f x))) x = (*h* g) ((*h* f) x)
[PROOF STEP]
proof (simp add: hyperdual_eq_iff, intro conjI disjI2)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
 2. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
 3. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
show goal1: "deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
[PROOF STEP]
have "deriv (\<lambda>x. g (f x)) (Base x) = deriv (g \<circ> f) (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv (g \<circ> f) (Base x)
[PROOF STEP]
by (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv (g \<circ> f) (Base x)

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv (g \<circ> f) (Base x)

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
[PROOF STEP]
have "... = deriv g (f (Base x)) * deriv f (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (g \<circ> f) (Base x) = deriv g (f (Base x)) * deriv f (Base x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
g twice_field_differentiable_at f (Base x)

goal (1 subgoal):
 1. deriv (g \<circ> f) (Base x) = deriv g (f (Base x)) * deriv f (Base x)
[PROOF STEP]
by (simp add: deriv_chain once_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
deriv (g \<circ> f) (Base x) = deriv g (f (Base x)) * deriv f (Base x)

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv g (f (Base x)) * deriv f (Base x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv g (f (Base x)) * deriv f (Base x)

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
[PROOF STEP]
by (simp add: mult.commute deriv_chain)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))

goal (2 subgoals):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
 2. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
[PROOF STEP]
show "deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))"
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))

goal (1 subgoal):
 1. deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. g (f x)) (Base x) = deriv f (Base x) * deriv g (f (Base x))

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
have first_diff: "(\<lambda>x. deriv g (f x)) field_differentiable at (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. deriv g (f x)) field_differentiable at (Base x)
[PROOF STEP]
by (metis DERIV_chain2 assms deriv_field_differentiable_at field_differentiable_def once_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. deriv g (f x)) field_differentiable at (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
have "deriv (deriv g \<circ> f) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv g \<circ> f) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)
[PROOF STEP]
using deriv_chain assms once_field_differentiable_at deriv_field_differentiable_at
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f field_differentiable at ?x; ?g field_differentiable at (?f ?x)\<rbrakk> \<Longrightarrow> deriv (?g \<circ> ?f) ?x = deriv ?g (?f ?x) * deriv ?f ?x
f twice_field_differentiable_at Base x
g twice_field_differentiable_at f (Base x)
?f twice_field_differentiable_at ?x \<Longrightarrow> ?f field_differentiable at ?x
?f twice_field_differentiable_at ?x \<Longrightarrow> deriv ?f field_differentiable at ?x

goal (1 subgoal):
 1. deriv (deriv g \<circ> f) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
deriv (deriv g \<circ> f) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (deriv g \<circ> f) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)
[PROOF STEP]
have deriv_deriv_comp: "deriv (\<lambda>x. deriv g (f x)) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)"
[PROOF STATE]
proof (prove)
using this:
deriv (deriv g \<circ> f) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)

goal (1 subgoal):
 1. deriv (\<lambda>x. deriv g (f x)) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)
[PROOF STEP]
by (simp add: comp_def)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. deriv g (f x)) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
have "deriv (deriv (\<lambda>x. g (f x))) (Base x) = deriv ((\<lambda>x. deriv f x * deriv g (f x))) (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. g (f x))) (Base x) = deriv (\<lambda>x. deriv f x * deriv g (f x)) (Base x)
[PROOF STEP]
using assms eventually_deriv_compose'[of f "Base x" g]
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
g twice_field_differentiable_at f (Base x)
\<lbrakk>f twice_field_differentiable_at Base x; g twice_field_differentiable_at f (Base x)\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in nhds (Base x). deriv (\<lambda>x. g (f x)) x = deriv g (f x) * deriv f x

goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. g (f x))) (Base x) = deriv (\<lambda>x. deriv f x * deriv g (f x)) (Base x)
[PROOF STEP]
by (simp add: mult.commute deriv_cong_ev)
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>x. g (f x))) (Base x) = deriv (\<lambda>x. deriv f x * deriv g (f x)) (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>x. g (f x))) (Base x) = deriv (\<lambda>x. deriv f x * deriv g (f x)) (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
have "... = deriv f (Base x) * deriv (\<lambda>x. deriv g (f x)) (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. deriv f x * deriv g (f x)) (Base x) = deriv f (Base x) * deriv (\<lambda>x. deriv g (f x)) (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))
[PROOF STEP]
using assms(1) first_diff
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
(\<lambda>x. deriv g (f x)) field_differentiable at (Base x)

goal (1 subgoal):
 1. deriv (\<lambda>x. deriv f x * deriv g (f x)) (Base x) = deriv f (Base x) * deriv (\<lambda>x. deriv g (f x)) (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))
[PROOF STEP]
by (simp add: deriv_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. deriv f x * deriv g (f x)) (Base x) = deriv f (Base x) * deriv (\<lambda>x. deriv g (f x)) (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. deriv f x * deriv g (f x)) (Base x) = deriv f (Base x) * deriv (\<lambda>x. deriv g (f x)) (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
have "... = deriv f (Base x) * deriv (deriv g) (f (Base x)) * deriv f (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv f (Base x) * deriv (\<lambda>x. deriv g (f x)) (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x)) = deriv f (Base x) * deriv (deriv g) (f (Base x)) * deriv f (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))
[PROOF STEP]
using deriv_deriv_comp
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. deriv g (f x)) (Base x) = deriv (deriv g) (f (Base x)) * deriv f (Base x)

goal (1 subgoal):
 1. deriv f (Base x) * deriv (\<lambda>x. deriv g (f x)) (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x)) = deriv f (Base x) * deriv (deriv g) (f (Base x)) * deriv f (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv f (Base x) * deriv (\<lambda>x. deriv g (f x)) (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x)) = deriv f (Base x) * deriv (deriv g) (f (Base x)) * deriv f (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
deriv (deriv (\<lambda>x. g (f x))) (Base x) = deriv f (Base x) * deriv (deriv g) (f (Base x)) * deriv f (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))
[PROOF STEP]
show "Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) =
    (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) +
    Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))"
[PROOF STATE]
proof (prove)
using this:
deriv (deriv (\<lambda>x. g (f x))) (Base x) = deriv f (Base x) * deriv (deriv g) (f (Base x)) * deriv f (Base x) + deriv (deriv f) (Base x) * deriv g (f (Base x))

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))
[PROOF STEP]
by (simp add: goal1 field_simps)
[PROOF STATE]
proof (state)
this:
Eps12 x * deriv (\<lambda>x. g (f x)) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. g (f x))) (Base x) = (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * deriv g (f (Base x)) + Eps1 x * deriv f (Base x) * (Eps2 x * deriv f (Base x)) * deriv (deriv g) (f (Base x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hypext_const [simp]:
  "(*h* (\<lambda>x. a)) x = of_comp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. a)) x = of_comp a
[PROOF STEP]
by (simp add: of_comp_def hyperdual_eq_iff)


[STATEMENT]
lemma "autodiff (\<lambda>x. a) = (\<lambda>x. Derivs a 0 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. autodiff (\<lambda>x. a) = (\<lambda>x. Derivs a (0::'a) (0::'a))
[PROOF STEP]
by simp


[STATEMENT]
lemma hypext_ident:
  "(*h* (\<lambda>x. x)) x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. x)) x = x
[PROOF STEP]
by (simp add: hyperdual_eq_iff)


[STATEMENT]
lemma hypext_scaleH:
  "(*h* (\<lambda>x. k * x)) x = k *\<^sub>H x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (*) k) x = k *\<^sub>H x
[PROOF STEP]
by (simp add: hyperdual_eq_iff)


[STATEMENT]
lemma hypext_fun_scaleH:
  assumes "f twice_field_differentiable_at (Base x)"
  shows "(*h* (\<lambda>x. k * f x)) x = k *\<^sub>H (*h* f) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. k * f x)) x = k *\<^sub>H (*h* f) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (*h* (\<lambda>x. k * f x)) x = k *\<^sub>H (*h* f) x
[PROOF STEP]
by (simp add: hypext_compose hypext_scaleH)


[STATEMENT]
lemma hypext_scaleR:
  "(*h* (\<lambda>x. k *\<^sub>R x)) x = k *\<^sub>R x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (*\<^sub>R) k) x = k *\<^sub>R x
[PROOF STEP]
by (auto simp add: hyperdual_eq_iff)


[STATEMENT]
lemma hypext_fun_scaleR:
  assumes "f twice_field_differentiable_at (Base x)"
  shows "(*h* (\<lambda>x. k *\<^sub>R f x)) x = k *\<^sub>R (*h* f) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. k *\<^sub>R f x)) x = k *\<^sub>R (*h* f) x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (*h* (\<lambda>x. k *\<^sub>R f x)) x = k *\<^sub>R (*h* f) x
[PROOF STEP]
by (simp add: hypext_compose hypext_scaleR)


[STATEMENT]
lemma hypext_fun_add:
  assumes "f twice_field_differentiable_at (Base x)"
      and "g twice_field_differentiable_at (Base x)"
    shows "(*h* (\<lambda>x. f x + g x)) x = (*h* f) x + (*h* g) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. f x + g x)) x = (*h* f) x + (*h* g) x
[PROOF STEP]
proof (simp add: hyperdual_eq_iff distrib_left[symmetric], intro conjI disjI2)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)
 2. deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)
 3. Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))
[PROOF STEP]
show goal1: "deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)
[PROOF STEP]
by (simp add: assms once_field_differentiable_at distrib_left)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)

goal (2 subgoals):
 1. deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)
 2. Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)
[PROOF STEP]
show "deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)"
[PROOF STATE]
proof (prove)
using this:
deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)

goal (1 subgoal):
 1. deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>x. f x + g x) (Base x) = deriv f (Base x) + deriv g (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))
[PROOF STEP]
have "deriv (deriv (\<lambda>x. f x + g x)) (Base x) = deriv (\<lambda>w. deriv f w + deriv g w) (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>x. f x + g x)) (Base x) = deriv (\<lambda>w. deriv f w + deriv g w) (Base x)
[PROOF STEP]
by (simp add: assms deriv_cong_ev eventually_deriv_add)
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>x. f x + g x)) (Base x) = deriv (\<lambda>w. deriv f w + deriv g w) (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>x. f x + g x)) (Base x) = deriv (\<lambda>w. deriv f w + deriv g w) (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))
[PROOF STEP]
have "Eps12 x * deriv f (Base x) + Eps12 x * deriv g (Base x) = Eps12 x * deriv (\<lambda>x. f x + g x) (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 x * deriv f (Base x) + Eps12 x * deriv g (Base x) = Eps12 x * deriv (\<lambda>x. f x + g x) (Base x)
[PROOF STEP]
by (metis distrib_left goal1)
[PROOF STATE]
proof (state)
this:
Eps12 x * deriv f (Base x) + Eps12 x * deriv g (Base x) = Eps12 x * deriv (\<lambda>x. f x + g x) (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
deriv (deriv (\<lambda>x. f x + g x)) (Base x) = deriv (\<lambda>w. deriv f w + deriv g w) (Base x)
Eps12 x * deriv f (Base x) + Eps12 x * deriv g (Base x) = Eps12 x * deriv (\<lambda>x. f x + g x) (Base x)
[PROOF STEP]
show "Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) +
    Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) =
    Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) +
    (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))"
[PROOF STATE]
proof (prove)
using this:
deriv (deriv (\<lambda>x. f x + g x)) (Base x) = deriv (\<lambda>w. deriv f w + deriv g w) (Base x)
Eps12 x * deriv f (Base x) + Eps12 x * deriv g (Base x) = Eps12 x * deriv (\<lambda>x. f x + g x) (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))
[PROOF STEP]
using deriv_add[OF deriv_field_differentiable_at deriv_field_differentiable_at, OF assms]
[PROOF STATE]
proof (prove)
using this:
deriv (deriv (\<lambda>x. f x + g x)) (Base x) = deriv (\<lambda>w. deriv f w + deriv g w) (Base x)
Eps12 x * deriv f (Base x) + Eps12 x * deriv g (Base x) = Eps12 x * deriv (\<lambda>x. f x + g x) (Base x)
deriv (\<lambda>w. deriv f w + deriv g w) (Base x) = deriv (deriv f) (Base x) + deriv (deriv g) (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))
[PROOF STEP]
by (simp add: distrib_left add.left_commute)
[PROOF STATE]
proof (state)
this:
Eps12 x * deriv (\<lambda>x. f x + g x) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>x. f x + g x)) (Base x) = Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x) + (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hypext_cadd [simp]:
  "(*h* (\<lambda>x. x + a)) x = x + of_comp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. x + a)) x = x + of_comp a
[PROOF STEP]
by (auto simp add: hyperdual_eq_iff of_comp_def)


[STATEMENT]
lemma hypext_fun_cadd:
  assumes "f twice_field_differentiable_at (Base x)"
  shows "(*h* (\<lambda>x. f x + a)) x = (*h* f) x + of_comp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. f x + a)) x = (*h* f) x + of_comp a
[PROOF STEP]
using assms hypext_compose[of f x "\<lambda>x. x + a"]
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
\<lbrakk>f twice_field_differentiable_at Base x; (\<lambda>x. x + a) twice_field_differentiable_at f (Base x)\<rbrakk> \<Longrightarrow> (*h* (\<lambda>x. f x + a)) x = (*h* (\<lambda>x. x + a)) ((*h* f) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. f x + a)) x = (*h* f) x + of_comp a
[PROOF STEP]
by simp


[STATEMENT]
lemma hypext_linear:
  "(*h* (\<lambda>x. k * x + a)) x = k *\<^sub>H x + of_comp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. k * x + a)) x = k *\<^sub>H x + of_comp a
[PROOF STEP]
using hypext_fun_add[of "(*) k" x "\<lambda>x. a"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(*) k twice_field_differentiable_at Base x; (\<lambda>x. a) twice_field_differentiable_at Base x\<rbrakk> \<Longrightarrow> (*h* (\<lambda>x. k * x + a)) x = (*h* (*) k) x + (*h* (\<lambda>x. a)) x

goal (1 subgoal):
 1. (*h* (\<lambda>x. k * x + a)) x = k *\<^sub>H x + of_comp a
[PROOF STEP]
by (simp add: hypext_scaleH)


[STATEMENT]
lemma hypext_fun_linear:
  assumes "f twice_field_differentiable_at (Base x)"
    shows "(*h* (\<lambda>x. k * f x + a)) x = k *\<^sub>H (*h* f) x + of_comp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. k * f x + a)) x = k *\<^sub>H (*h* f) x + of_comp a
[PROOF STEP]
using assms hypext_compose[of f x "\<lambda>x. k * x + a"]
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
\<lbrakk>f twice_field_differentiable_at Base x; (\<lambda>x. k * x + a) twice_field_differentiable_at f (Base x)\<rbrakk> \<Longrightarrow> (*h* (\<lambda>x. k * f x + a)) x = (*h* (\<lambda>x. k * x + a)) ((*h* f) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. k * f x + a)) x = k *\<^sub>H (*h* f) x + of_comp a
[PROOF STEP]
by (simp add: hypext_linear)


[STATEMENT]
lemma hypext_linearR:
  "(*h* (\<lambda>x. k *\<^sub>R x + a)) x = k *\<^sub>R x + of_comp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. k *\<^sub>R x + a)) x = k *\<^sub>R x + of_comp a
[PROOF STEP]
using hypext_fun_add[of "(*\<^sub>R) k" x "\<lambda>x. a"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(*\<^sub>R) k twice_field_differentiable_at Base x; (\<lambda>x. a) twice_field_differentiable_at Base x\<rbrakk> \<Longrightarrow> (*h* (\<lambda>x. k *\<^sub>R x + a)) x = (*h* (*\<^sub>R) k) x + (*h* (\<lambda>x. a)) x

goal (1 subgoal):
 1. (*h* (\<lambda>x. k *\<^sub>R x + a)) x = k *\<^sub>R x + of_comp a
[PROOF STEP]
by (simp add: hypext_scaleR)


[STATEMENT]
lemma hypext_fun_linearR:
  assumes "f twice_field_differentiable_at (Base x)"
    shows "(*h* (\<lambda>x. k *\<^sub>R f x + a)) x = k *\<^sub>R (*h* f) x + of_comp a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. k *\<^sub>R f x + a)) x = k *\<^sub>R (*h* f) x + of_comp a
[PROOF STEP]
using assms hypext_compose[of f x "\<lambda>x. k *\<^sub>R x + a"]
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
\<lbrakk>f twice_field_differentiable_at Base x; (\<lambda>x. k *\<^sub>R x + a) twice_field_differentiable_at f (Base x)\<rbrakk> \<Longrightarrow> (*h* (\<lambda>x. k *\<^sub>R f x + a)) x = (*h* (\<lambda>x. k *\<^sub>R x + a)) ((*h* f) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. k *\<^sub>R f x + a)) x = k *\<^sub>R (*h* f) x + of_comp a
[PROOF STEP]
by (simp add: hypext_linearR)


[STATEMENT]
lemma hypext_fun_mult:
  assumes "f twice_field_differentiable_at (Base x)"
      and "g twice_field_differentiable_at (Base x)"
    shows "(*h* (\<lambda>z. f z * g z)) x = (*h* f) x * (*h* g) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>z. f z * g z)) x = (*h* f) x * (*h* g) x
[PROOF STEP]
proof (simp add: hyperdual_eq_iff distrib_left[symmetric], intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Eps1 x * deriv (\<lambda>z. f z * g z) (Base x) = f (Base x) * (Eps1 x * deriv g (Base x)) + Eps1 x * deriv f (Base x) * g (Base x)
 2. Eps2 x * deriv (\<lambda>z. f z * g z) (Base x) = f (Base x) * (Eps2 x * deriv g (Base x)) + Eps2 x * deriv f (Base x) * g (Base x)
 3. Eps12 x * deriv (\<lambda>z. f z * g z) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>z. f z * g z)) (Base x) = (2::'a) * (Eps1 x * (Eps2 x * (deriv f (Base x) * deriv g (Base x)))) + f (Base x) * (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x)) + (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * g (Base x)
[PROOF STEP]
show "Eps1 x * deriv (\<lambda>z. f z * g z) (Base x) =
        f (Base x) * (Eps1 x * deriv g (Base x)) + Eps1 x * deriv f (Base x) * g (Base x)"
   and "Eps2 x * deriv (\<lambda>z. f z * g z) (Base x) =
        f (Base x) * (Eps2 x * deriv g (Base x)) + Eps2 x * deriv f (Base x) * g (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps1 x * deriv (\<lambda>z. f z * g z) (Base x) = f (Base x) * (Eps1 x * deriv g (Base x)) + Eps1 x * deriv f (Base x) * g (Base x) &&& Eps2 x * deriv (\<lambda>z. f z * g z) (Base x) = f (Base x) * (Eps2 x * deriv g (Base x)) + Eps2 x * deriv f (Base x) * g (Base x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
g twice_field_differentiable_at Base x

goal (1 subgoal):
 1. Eps1 x * deriv (\<lambda>z. f z * g z) (Base x) = f (Base x) * (Eps1 x * deriv g (Base x)) + Eps1 x * deriv f (Base x) * g (Base x) &&& Eps2 x * deriv (\<lambda>z. f z * g z) (Base x) = f (Base x) * (Eps2 x * deriv g (Base x)) + Eps2 x * deriv f (Base x) * g (Base x)
[PROOF STEP]
by (simp_all add: once_field_differentiable_at distrib_left)
[PROOF STATE]
proof (state)
this:
Eps1 x * deriv (\<lambda>z. f z * g z) (Base x) = f (Base x) * (Eps1 x * deriv g (Base x)) + Eps1 x * deriv f (Base x) * g (Base x)
Eps2 x * deriv (\<lambda>z. f z * g z) (Base x) = f (Base x) * (Eps2 x * deriv g (Base x)) + Eps2 x * deriv f (Base x) * g (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>z. f z * g z) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>z. f z * g z)) (Base x) = (2::'a) * (Eps1 x * (Eps2 x * (deriv f (Base x) * deriv g (Base x)))) + f (Base x) * (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x)) + (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * g (Base x)
[PROOF STEP]
have
    "deriv (deriv (\<lambda>z. f z * g z)) (Base x) =
     f (Base x) * deriv (deriv g) (Base x) + 2 * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
have "deriv (deriv (\<lambda>z. f z * g z)) (Base x) = deriv (\<lambda>z. f z * deriv g z + deriv f z * g z) (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (deriv (\<lambda>z. f z * g z)) (Base x) = deriv (\<lambda>z. f z * deriv g z + deriv f z * g z) (Base x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
g twice_field_differentiable_at Base x

goal (1 subgoal):
 1. deriv (deriv (\<lambda>z. f z * g z)) (Base x) = deriv (\<lambda>z. f z * deriv g z + deriv f z * g z) (Base x)
[PROOF STEP]
by (simp add: eventually_deriv_mult deriv_cong_ev)
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = deriv (\<lambda>z. f z * deriv g z + deriv f z * g z) (Base x)

goal (1 subgoal):
 1. deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = deriv (\<lambda>z. f z * deriv g z + deriv f z * g z) (Base x)

goal (1 subgoal):
 1. deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
have "... = (\<lambda>z. f z * deriv (deriv g) z + deriv f z * deriv g z + deriv f z * deriv g z + deriv (deriv f) z * g z) (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv (\<lambda>z. f z * deriv g z + deriv f z * g z) (Base x) = f (Base x) * deriv (deriv g) (Base x) + deriv f (Base x) * deriv g (Base x) + deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
by (simp add: assms deriv_field_differentiable_at field_differentiable_mult once_field_differentiable_at)
[PROOF STATE]
proof (state)
this:
deriv (\<lambda>z. f z * deriv g z + deriv f z * g z) (Base x) = f (Base x) * deriv (deriv g) (Base x) + deriv f (Base x) * deriv g (Base x) + deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)

goal (1 subgoal):
 1. deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + deriv f (Base x) * deriv g (Base x) + deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + deriv f (Base x) * deriv g (Base x) + deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)

goal (1 subgoal):
 1. deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>z. f z * g z) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>z. f z * g z)) (Base x) = (2::'a) * (Eps1 x * (Eps2 x * (deriv f (Base x) * deriv g (Base x)))) + f (Base x) * (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x)) + (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * g (Base x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
[PROOF STEP]
show
    "Eps12 x * deriv (\<lambda>z. f z * g z) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>z. f z * g z)) (Base x) =
     2 * (Eps1 x * (Eps2 x * (deriv f (Base x) * deriv g (Base x)))) +
     f (Base x) * (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x)) +
     (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * g (Base x)"
[PROOF STATE]
proof (prove)
using this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>z. f z * g z) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>z. f z * g z)) (Base x) = (2::'a) * (Eps1 x * (Eps2 x * (deriv f (Base x) * deriv g (Base x)))) + f (Base x) * (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x)) + (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * g (Base x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
deriv (deriv (\<lambda>z. f z * g z)) (Base x) = f (Base x) * deriv (deriv g) (Base x) + (2::'a) * deriv f (Base x) * deriv g (Base x) + deriv (deriv f) (Base x) * g (Base x)
f twice_field_differentiable_at Base x
g twice_field_differentiable_at Base x

goal (1 subgoal):
 1. Eps12 x * deriv (\<lambda>z. f z * g z) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>z. f z * g z)) (Base x) = (2::'a) * (Eps1 x * (Eps2 x * (deriv f (Base x) * deriv g (Base x)))) + f (Base x) * (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x)) + (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * g (Base x)
[PROOF STEP]
by (simp add: once_field_differentiable_at field_simps)
[PROOF STATE]
proof (state)
this:
Eps12 x * deriv (\<lambda>z. f z * g z) (Base x) + Eps1 x * Eps2 x * deriv (deriv (\<lambda>z. f z * g z)) (Base x) = (2::'a) * (Eps1 x * (Eps2 x * (deriv f (Base x) * deriv g (Base x)))) + f (Base x) * (Eps12 x * deriv g (Base x) + Eps1 x * Eps2 x * deriv (deriv g) (Base x)) + (Eps12 x * deriv f (Base x) + Eps1 x * Eps2 x * deriv (deriv f) (Base x)) * g (Base x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hypext_sin_Hyperdual:
  "(*h* sin) (Hyperdual a b c d) = sin a *\<^sub>H ba + (b *cos a) *\<^sub>H e1 + (c * cos a) *\<^sub>H e2 + (d * cos a - b * c * sin a) *\<^sub>H e12 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* sin) (Hyperdual a b c d) = sin a *\<^sub>H ba + (b * cos a) *\<^sub>H e1 + (c * cos a) *\<^sub>H e2 + (d * cos a - b * c * sin a) *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_Hyperdual_eq_parts)


[STATEMENT]
lemma hypext_cos_Hyperdual:
  "(*h* cos) (Hyperdual a b c d) = cos a *\<^sub>H ba - (b * sin a) *\<^sub>H e1 - (c * sin a) *\<^sub>H e2 - (d * sin a + b * c * cos a) *\<^sub>H e12 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* cos) (Hyperdual a b c d) = cos a *\<^sub>H ba - (b * sin a) *\<^sub>H e1 - (c * sin a) *\<^sub>H e2 - (d * sin a + b * c * cos a) *\<^sub>H e12
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (*h* cos) (Hyperdual a b c d) = cos a *\<^sub>H ba - (b * sin a) *\<^sub>H e1 - (c * sin a) *\<^sub>H e2 - (d * sin a + b * c * cos a) *\<^sub>H e12
[PROOF STEP]
have "of_comp (- (d * sin a) - b * c * cos a) * e12 = - (of_comp (d * sin a + b * c * cos a) * e12)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_comp (- (d * sin a) - b * c * cos a) * e12 = - (of_comp (d * sin a + b * c * cos a) * e12)
[PROOF STEP]
by (metis add_uminus_conv_diff minus_add_distrib mult_minus_left of_comp_minus)
[PROOF STATE]
proof (state)
this:
of_comp (- (d * sin a) - b * c * cos a) * e12 = - (of_comp (d * sin a + b * c * cos a) * e12)

goal (1 subgoal):
 1. (*h* cos) (Hyperdual a b c d) = cos a *\<^sub>H ba - (b * sin a) *\<^sub>H e1 - (c * sin a) *\<^sub>H e2 - (d * sin a + b * c * cos a) *\<^sub>H e12
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
of_comp (- (d * sin a) - b * c * cos a) * e12 = - (of_comp (d * sin a + b * c * cos a) * e12)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_comp (- (d * sin a) - b * c * cos a) * e12 = - (of_comp (d * sin a + b * c * cos a) * e12)

goal (1 subgoal):
 1. (*h* cos) (Hyperdual a b c d) = cos a *\<^sub>H ba - (b * sin a) *\<^sub>H e1 - (c * sin a) *\<^sub>H e2 - (d * sin a + b * c * cos a) *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_Hyperdual_eq_parts of_comp_minus scaleH_times)
[PROOF STATE]
proof (state)
this:
(*h* cos) (Hyperdual a b c d) = cos a *\<^sub>H ba - (b * sin a) *\<^sub>H e1 - (c * sin a) *\<^sub>H e2 - (d * sin a + b * c * cos a) *\<^sub>H e12

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Eps1_hypext_sin [simp]:
  "Eps1 ((*h* sin) x) = Eps1 x * cos (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps1 ((*h* sin) x) = Eps1 x * cos (Base x)
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps2_hypext_sin [simp]:
  "Eps2 ((*h* sin) x) = Eps2 x * cos (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps2 ((*h* sin) x) = Eps2 x * cos (Base x)
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps12_hypext_sin [simp]:
  "Eps12 ((*h* sin) x) = Eps12 x * cos (Base x) - Eps1 x * Eps2 x * sin (Base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 ((*h* sin) x) = Eps12 x * cos (Base x) - Eps1 x * Eps2 x * sin (Base x)
[PROOF STEP]
by simp


[STATEMENT]
lemma hypext_sin_e1 [simp]:
  "(*h* sin) (x * e1) = e1 * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* sin) (x * e1) = e1 * x
[PROOF STEP]
by (simp add: e1_def hyperdual_eq_iff one_hyperdual_def)


[STATEMENT]
lemma hypext_sin_e2 [simp]:
  "(*h* sin) (x * e2) = e2 * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* sin) (x * e2) = e2 * x
[PROOF STEP]
by (simp add: e2_def hyperdual_eq_iff one_hyperdual_def)


[STATEMENT]
lemma hypext_sin_e12 [simp]:
  "(*h* sin) (x * e12) = e12 * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* sin) (x * e12) = e12 * x
[PROOF STEP]
by (simp add: e12_def hyperdual_eq_iff one_hyperdual_def)


[STATEMENT]
lemma hypext_cos_e1 [simp]:
  "(*h* cos) (x * e1) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* cos) (x * e1) = 1
[PROOF STEP]
by (simp add: e1_def hyperdual_eq_iff one_hyperdual_def)


[STATEMENT]
lemma hypext_cos_e2 [simp]:
  "(*h* cos) (x * e2) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* cos) (x * e2) = 1
[PROOF STEP]
by (simp add: e2_def hyperdual_eq_iff one_hyperdual_def)


[STATEMENT]
lemma hypext_cos_e12 [simp]:
  "(*h* cos) (x * e12) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* cos) (x * e12) = 1
[PROOF STEP]
by (simp add: e12_def hyperdual_eq_iff one_hyperdual_def)


[STATEMENT]
lemma hypext_sin_extract:
  "(*h* sin) (\<beta> x) = sin x *\<^sub>H ba + cos x *\<^sub>H e1 + cos x *\<^sub>H e2 - sin x *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* sin) (\<beta> x) = sin x *\<^sub>H ba + cos x *\<^sub>H e1 + cos x *\<^sub>H e2 - sin x *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_sin_Hyperdual of_comp_minus scaleH_times hyperdualx_def)


[STATEMENT]
lemma hypext_cos_extract:
  "(*h* cos) (\<beta> x) = cos x *\<^sub>H ba - sin x *\<^sub>H e1 - sin x *\<^sub>H e2 - cos x *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* cos) (\<beta> x) = cos x *\<^sub>H ba - sin x *\<^sub>H e1 - sin x *\<^sub>H e2 - cos x *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_cos_Hyperdual hyperdualx_def)


[STATEMENT]
lemma Base_hypext_sin_extract [simp]:
  "Base ((*h* sin) (\<beta> x)) = sin x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Base ((*h* sin) (\<beta> x)) = sin x
[PROOF STEP]
by (rule Base_hypext)


[STATEMENT]
lemma Eps2_hypext_sin_extract [simp]:
  "Eps2 ((*h* sin) (\<beta> x)) = cos x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps2 ((*h* sin) (\<beta> x)) = cos x
[PROOF STEP]
using Eps2_hypext[of sin]
[PROOF STATE]
proof (prove)
using this:
Eps2 ((*h* sin) (\<beta> ?x)) = deriv sin ?x

goal (1 subgoal):
 1. Eps2 ((*h* sin) (\<beta> x)) = cos x
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps12_hypext_sin_extract [simp]:
  "Eps12 ((*h* sin) (\<beta> x)) = - sin x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 ((*h* sin) (\<beta> x)) = - sin x
[PROOF STEP]
using Eps12_hypext[of sin]
[PROOF STATE]
proof (prove)
using this:
Eps12 ((*h* sin) (\<beta> ?x)) = deriv (deriv sin) ?x

goal (1 subgoal):
 1. Eps12 ((*h* sin) (\<beta> x)) = - sin x
[PROOF STEP]
by simp


[STATEMENT]
lemma Base_hypext_cos_extract [simp]:
  "Base ((*h* cos) (\<beta> x)) = cos x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Base ((*h* cos) (\<beta> x)) = cos x
[PROOF STEP]
by (rule Base_hypext)


[STATEMENT]
lemma Eps2_hypext_cos_extract [simp]:
  "Eps2 ((*h* cos) (\<beta> x)) = - sin x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps2 ((*h* cos) (\<beta> x)) = - sin x
[PROOF STEP]
using Eps2_hypext[of cos]
[PROOF STATE]
proof (prove)
using this:
Eps2 ((*h* cos) (\<beta> ?x)) = deriv cos ?x

goal (1 subgoal):
 1. Eps2 ((*h* cos) (\<beta> x)) = - sin x
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps12_hypext_cos_extract [simp]:
  "Eps12 ((*h* cos) (\<beta> x)) = - cos x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 ((*h* cos) (\<beta> x)) = - cos x
[PROOF STEP]
using Eps12_hypext[of cos]
[PROOF STATE]
proof (prove)
using this:
Eps12 ((*h* cos) (\<beta> ?x)) = deriv (deriv cos) ?x

goal (1 subgoal):
 1. Eps12 ((*h* cos) (\<beta> x)) = - cos x
[PROOF STEP]
by simp


[STATEMENT]
lemma "((*h* sin) x)\<^sup>2 + ((*h* cos) x)\<^sup>2 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((*h* sin) x)\<^sup>2 + ((*h* cos) x)\<^sup>2 = 1
[PROOF STEP]
by (simp add: hyperdual_eq_iff one_hyperdual_def power2_eq_square field_simps)


[STATEMENT]
lemma "(*h* sin) x + (*h* cos) x = (*h* (\<lambda>x. sin x + cos x)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* sin) x + (*h* cos) x = (*h* (\<lambda>x. sin x + cos x)) x
[PROOF STEP]
by (simp add: hypext_fun_add)


[STATEMENT]
lemma hypext_exp_Hyperdual:
  "(*h* exp) (Hyperdual a b c d) =
       exp a *\<^sub>H ba + (b * exp a) *\<^sub>H e1 + (c * exp a) *\<^sub>H e2 + (d * exp a + b * c * exp a) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* exp) (Hyperdual a b c d) = exp a *\<^sub>H ba + (b * exp a) *\<^sub>H e1 + (c * exp a) *\<^sub>H e2 + (d * exp a + b * c * exp a) *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_Hyperdual_eq_parts)


[STATEMENT]
lemma hypext_exp_extract:
  "(*h* exp) (\<beta> x) = exp x *\<^sub>H ba + exp x *\<^sub>H e1 + exp x *\<^sub>H e2 + exp x *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* exp) (\<beta> x) = exp x *\<^sub>H ba + exp x *\<^sub>H e1 + exp x *\<^sub>H e2 + exp x *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_extract_eq)


[STATEMENT]
lemma hypext_exp_e1 [simp]:
  "(*h* exp) (x * e1) = 1 + e1 * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* exp) (x * e1) = 1 + e1 * x
[PROOF STEP]
by (simp add: e1_def hyperdual_eq_iff)


[STATEMENT]
lemma hypext_exp_e2 [simp]:
  "(*h* exp) (x * e2) = 1 + e2 * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* exp) (x * e2) = 1 + e2 * x
[PROOF STEP]
by (simp add: e2_def hyperdual_eq_iff)


[STATEMENT]
lemma hypext_exp_e12 [simp]:
  "(*h* exp) (x * e12) = 1 + e12 * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* exp) (x * e12) = 1 + e12 * x
[PROOF STEP]
by (simp add: e12_def hyperdual_eq_iff)


[STATEMENT]
lemma Eps1_hypext_exp_extract [simp]:
  "Eps1 ((*h* exp) (\<beta> x)) = exp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps1 ((*h* exp) (\<beta> x)) = exp x
[PROOF STEP]
using Eps1_hypext[of exp]
[PROOF STATE]
proof (prove)
using this:
Eps1 ((*h* exp) (\<beta> ?x)) = deriv exp ?x

goal (1 subgoal):
 1. Eps1 ((*h* exp) (\<beta> x)) = exp x
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps2_hypext_exp_extract [simp]:
  "Eps2 ((*h* exp) (\<beta> x)) = exp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps2 ((*h* exp) (\<beta> x)) = exp x
[PROOF STEP]
using Eps2_hypext[of exp]
[PROOF STATE]
proof (prove)
using this:
Eps2 ((*h* exp) (\<beta> ?x)) = deriv exp ?x

goal (1 subgoal):
 1. Eps2 ((*h* exp) (\<beta> x)) = exp x
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps12_hypext_exp_extract [simp]:
  "Eps12 ((*h* exp) (\<beta> x)) = exp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 ((*h* exp) (\<beta> x)) = exp x
[PROOF STEP]
using Eps12_hypext[of exp]
[PROOF STATE]
proof (prove)
using this:
Eps12 ((*h* exp) (\<beta> ?x)) = deriv (deriv exp) ?x

goal (1 subgoal):
 1. Eps12 ((*h* exp) (\<beta> x)) = exp x
[PROOF STEP]
by simp


[STATEMENT]
lemma hypext_sqrt_Hyperdual_Hyperdual:
  assumes "a > 0"
  shows "(*h* sqrt) (Hyperdual a b c d) =
         Hyperdual (sqrt a) (b * inverse (sqrt a) / 2) (c * inverse (sqrt a) / 2)
           (d * inverse (sqrt a) / 2 - b * c * inverse (sqrt a ^ 3) / 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* sqrt) (Hyperdual a b c d) = Hyperdual (sqrt a) (b * inverse (sqrt a) / 2) (c * inverse (sqrt a) / 2) (d * inverse (sqrt a) / 2 - b * c * inverse (sqrt a ^ 3) / 4)
[PROOF STEP]
by (simp add: assms hypext_Hyperdual_eq)


[STATEMENT]
lemma hypext_sqrt_Hyperdual:
      "a > 0 \<Longrightarrow> (*h* sqrt) (Hyperdual a b c d) =
       sqrt a *\<^sub>H ba + (b * inverse (sqrt a) / 2) *\<^sub>H e1 + (c * inverse (sqrt a) / 2) *\<^sub>H e2 +
       (d * inverse (sqrt a) / 2 - b * c * inverse (sqrt a ^ 3) / 4) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < a \<Longrightarrow> (*h* sqrt) (Hyperdual a b c d) = sqrt a *\<^sub>H ba + (b * inverse (sqrt a) / 2) *\<^sub>H e1 + (c * inverse (sqrt a) / 2) *\<^sub>H e2 + (d * inverse (sqrt a) / 2 - b * c * inverse (sqrt a ^ 3) / 4) *\<^sub>H e12
[PROOF STEP]
by (auto simp add: hypext_Hyperdual_eq_parts)


[STATEMENT]
lemma hypext_sqrt_extract:
  "x > 0 \<Longrightarrow> (*h* sqrt) (\<beta> x) = sqrt x *\<^sub>H ba + (inverse (sqrt x) / 2) *\<^sub>H e1 +
        (inverse (sqrt x) / 2) *\<^sub>H e2 - (inverse (sqrt x ^ 3) / 4) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> (*h* sqrt) (\<beta> x) = sqrt x *\<^sub>H ba + (inverse (sqrt x) / 2) *\<^sub>H e1 + (inverse (sqrt x) / 2) *\<^sub>H e2 - (inverse (sqrt x ^ 3) / 4) *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_sqrt_Hyperdual hyperdualx_def of_comp_minus scaleH_times)


[STATEMENT]
lemma Eps1_hypext_sqrt_extract [simp]:
  "x > 0 \<Longrightarrow> Eps1 ((*h* sqrt) (\<beta> x)) = inverse (sqrt x) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> Eps1 ((*h* sqrt) (\<beta> x)) = inverse (sqrt x) / 2
[PROOF STEP]
using Eps1_hypext[of sqrt]
[PROOF STATE]
proof (prove)
using this:
Eps1 ((*h* sqrt) (\<beta> ?x)) = deriv sqrt ?x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> Eps1 ((*h* sqrt) (\<beta> x)) = inverse (sqrt x) / 2
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps2_hypext_sqrt_extract [simp]:
  "x > 0 \<Longrightarrow> Eps2 ((*h* sqrt) (\<beta> x)) = inverse (sqrt x) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> Eps2 ((*h* sqrt) (\<beta> x)) = inverse (sqrt x) / 2
[PROOF STEP]
using Eps2_hypext[of sqrt]
[PROOF STATE]
proof (prove)
using this:
Eps2 ((*h* sqrt) (\<beta> ?x)) = deriv sqrt ?x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> Eps2 ((*h* sqrt) (\<beta> x)) = inverse (sqrt x) / 2
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps12_hypext_sqrt_extract [simp]:
  "x > 0 \<Longrightarrow> Eps12 ((*h* sqrt) (\<beta> x)) = - (inverse (sqrt x ^ 3) / 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> Eps12 ((*h* sqrt) (\<beta> x)) = - (inverse (sqrt x ^ 3) / 4)
[PROOF STEP]
using Eps12_hypext[of sqrt]
[PROOF STATE]
proof (prove)
using this:
Eps12 ((*h* sqrt) (\<beta> ?x)) = deriv (deriv sqrt) ?x

goal (1 subgoal):
 1. 0 < x \<Longrightarrow> Eps12 ((*h* sqrt) (\<beta> x)) = - (inverse (sqrt x ^ 3) / 4)
[PROOF STEP]
by simp


[STATEMENT]
lemma "Base x > 0 \<Longrightarrow> (*h* sin) x + (*h* sqrt) x = (*h* (\<lambda>x. sin x + sqrt x)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Base x \<Longrightarrow> (*h* sin) x + (*h* sqrt) x = (*h* (\<lambda>x. sin x + sqrt x)) x
[PROOF STEP]
by (simp add: hypext_fun_add)


[STATEMENT]
lemma hypext_power:
  "(*h* (\<lambda>x. x ^ n)) x = x ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. x ^ n)) x = x ^ n
[PROOF STEP]
by (simp add: hyperdual_eq_iff hyperdual_power)


[STATEMENT]
lemma hypext_fun_power:
  assumes "f twice_field_differentiable_at (Base x)"
    shows "(*h* (\<lambda>x. (f x) ^ n)) x = ((*h* f) x) ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. f x ^ n)) x = (*h* f) x ^ n
[PROOF STEP]
using assms hypext_compose[of f x "\<lambda>x. x ^ n"]
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
\<lbrakk>f twice_field_differentiable_at Base x; (\<lambda>x. x ^ n) twice_field_differentiable_at f (Base x)\<rbrakk> \<Longrightarrow> (*h* (\<lambda>x. f x ^ n)) x = (*h* (\<lambda>x. x ^ n)) ((*h* f) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. f x ^ n)) x = (*h* f) x ^ n
[PROOF STEP]
by (simp add: hypext_power)


[STATEMENT]
lemma hypext_power_Hyperdual:
  "(*h* (\<lambda>x. x ^ n)) (Hyperdual a b c d) =
        a ^ n *\<^sub>H ba + (of_nat n * b * a ^ (n - 1)) *\<^sub>H e1 + (of_nat n * c * a ^ (n - 1)) *\<^sub>H e2 +
        (d * (of_nat n * a ^ (n - 1)) + b * c * (of_nat n * of_nat (n - 1) * a ^ (n - 2))) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. x ^ n)) (Hyperdual a b c d) = a ^ n *\<^sub>H ba + (of_nat n * b * a ^ (n - 1)) *\<^sub>H e1 + (of_nat n * c * a ^ (n - 1)) *\<^sub>H e2 + (d * (of_nat n * a ^ (n - 1)) + b * c * (of_nat n * of_nat (n - 1) * a ^ (n - 2))) *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_Hyperdual_eq_parts algebra_simps)


[STATEMENT]
lemma hypext_power_Hyperdual_parts:
  "(*h* (\<lambda>x. x ^ n)) (a *\<^sub>H ba + b *\<^sub>H e1 + c *\<^sub>H e2 + d *\<^sub>H e12) =
        a ^ n *\<^sub>H ba + (of_nat n * b * a ^ (n - 1)) *\<^sub>H e1 + (of_nat n * c * a ^ (n - 1)) *\<^sub>H e2 +
        (d * (of_nat n * a ^ (n - 1)) + b * c * (of_nat n * of_nat (n - 1) * a ^ (n - 2))) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. x ^ n)) (a *\<^sub>H ba + b *\<^sub>H e1 + c *\<^sub>H e2 + d *\<^sub>H e12) = a ^ n *\<^sub>H ba + (of_nat n * b * a ^ (n - 1)) *\<^sub>H e1 + (of_nat n * c * a ^ (n - 1)) *\<^sub>H e2 + (d * (of_nat n * a ^ (n - 1)) + b * c * (of_nat n * of_nat (n - 1) * a ^ (n - 2))) *\<^sub>H e12
[PROOF STEP]
by (simp add: Hyperdual_eq [symmetric] hypext_power_Hyperdual)


[STATEMENT]
lemma hypext_power_extract:
  "(*h* (\<lambda>x. x ^ n)) (\<beta> x) =
      x ^ n *\<^sub>H ba + (of_nat n * x ^ (n - 1)) *\<^sub>H e1 + (of_nat n * x ^ (n - 1)) *\<^sub>H e2 +
      (of_nat n * of_nat (n - 1) * x ^ (n - 2)) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. x ^ n)) (\<beta> x) = x ^ n *\<^sub>H ba + (of_nat n * x ^ (n - 1)) *\<^sub>H e1 + (of_nat n * x ^ (n - 1)) *\<^sub>H e2 + (of_nat n * of_nat (n - 1) * x ^ (n - 2)) *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_extract_eq)


[STATEMENT]
lemma Eps1_hypext_power [simp]:
  "Eps1 ((*h* (\<lambda>x. x ^ n)) x) = of_nat n * Eps1 x * (Base x) ^ (n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps1 ((*h* (\<lambda>x. x ^ n)) x) = of_nat n * Eps1 x * Base x ^ (n - 1)
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps2_hypext_power [simp]:
  "Eps2 ((*h* (\<lambda>x. x ^ n)) x) = of_nat n * Eps2 x * (Base x) ^ (n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps2 ((*h* (\<lambda>x. x ^ n)) x) = of_nat n * Eps2 x * Base x ^ (n - 1)
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps12_hypext_power [simp]:
  "Eps12 ((*h* (\<lambda>x. x ^ n)) x) =
   Eps12 x * (of_nat n * Base x ^ (n - 1)) + Eps1 x * Eps2 x * (of_nat n * of_nat (n - 1) * Base x ^ (n - 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Eps12 ((*h* (\<lambda>x. x ^ n)) x) = Eps12 x * (of_nat n * Base x ^ (n - 1)) + Eps1 x * Eps2 x * (of_nat n * of_nat (n - 1) * Base x ^ (n - 2))
[PROOF STEP]
by simp


[STATEMENT]
lemma hypext_inverse:
  assumes "Base x \<noteq> 0"
  shows "(*h* inverse) x = inverse x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* inverse) x = inverse x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Base x \<noteq> (0::'a)

goal (1 subgoal):
 1. (*h* inverse) x = inverse x
[PROOF STEP]
by (simp add: hyperdual_eq_iff inverse_eq_divide)


[STATEMENT]
lemma hypext_fun_inverse:
  assumes "f twice_field_differentiable_at (Base x)"
      and "f (Base x) \<noteq> 0"
    shows "(*h* (\<lambda>x. inverse (f x))) x = inverse ((*h* f) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. inverse (f x))) x = inverse ((*h* f) x)
[PROOF STEP]
using assms hypext_compose[of f x inverse]
[PROOF STATE]
proof (prove)
using this:
f twice_field_differentiable_at Base x
f (Base x) \<noteq> (0::'a)
\<lbrakk>f twice_field_differentiable_at Base x; inverse twice_field_differentiable_at f (Base x)\<rbrakk> \<Longrightarrow> (*h* (\<lambda>x. inverse (f x))) x = (*h* inverse) ((*h* f) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. inverse (f x))) x = inverse ((*h* f) x)
[PROOF STEP]
by (simp add: hypext_inverse)


[STATEMENT]
lemma hypext_inverse_Hyperdual:
  "a \<noteq> 0 \<Longrightarrow>
    (*h* inverse) (Hyperdual a b c d) =
    Hyperdual (inverse a) (- (b / a\<^sup>2)) (- (c / a\<^sup>2)) (2 * b * c / (a ^ 3) - d / a\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> (*h* inverse) (Hyperdual a b c d) = Hyperdual (inverse a) (- (b / a\<^sup>2)) (- (c / a\<^sup>2)) ((2::'a) * b * c / a ^ 3 - d / a\<^sup>2)
[PROOF STEP]
by (simp add: hypext_Hyperdual_eq divide_inverse)


[STATEMENT]
lemma hypext_inverse_Hyperdual_parts:
  "a \<noteq> 0 \<Longrightarrow>
    (*h* inverse) (a *\<^sub>H ba + b *\<^sub>H e1 + c *\<^sub>H e2 + d *\<^sub>H e12) =
    inverse a *\<^sub>H ba + - (b / a\<^sup>2) *\<^sub>H e1 + - (c / a\<^sup>2) *\<^sub>H e2 + (2 * b * c / a ^ 3 - d / a\<^sup>2) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> (*h* inverse) (a *\<^sub>H ba + b *\<^sub>H e1 + c *\<^sub>H e2 + d *\<^sub>H e12) = inverse a *\<^sub>H ba + - (b / a\<^sup>2) *\<^sub>H e1 + - (c / a\<^sup>2) *\<^sub>H e2 + ((2::'a) * b * c / a ^ 3 - d / a\<^sup>2) *\<^sub>H e12
[PROOF STEP]
by (metis Hyperdual_eq hypext_inverse_Hyperdual)


[STATEMENT]
lemma inverse_Hyperdual_parts:
  "(a::'a::real_normed_field) \<noteq> 0 \<Longrightarrow>
    inverse (a *\<^sub>H ba + b *\<^sub>H e1 + c *\<^sub>H e2 + d *\<^sub>H e12) =
    inverse a *\<^sub>H ba + - (b / a\<^sup>2) *\<^sub>H e1 + - (c / a\<^sup>2) *\<^sub>H e2 + (2 * b * c / a ^ 3 - d / a\<^sup>2) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (0::'a) \<Longrightarrow> inverse (a *\<^sub>H ba + b *\<^sub>H e1 + c *\<^sub>H e2 + d *\<^sub>H e12) = inverse a *\<^sub>H ba + - (b / a\<^sup>2) *\<^sub>H e1 + - (c / a\<^sup>2) *\<^sub>H e2 + ((2::'a) * b * c / a ^ 3 - d / a\<^sup>2) *\<^sub>H e12
[PROOF STEP]
by (metis Hyperdual_eq hyperdual.sel(1) hypext_inverse hypext_inverse_Hyperdual_parts)


[STATEMENT]
lemma hypext_inverse_extract:
  "x \<noteq> 0 \<Longrightarrow> (*h* inverse) (\<beta> x) = inverse x *\<^sub>H ba - (1 / x\<^sup>2) *\<^sub>H e1 - (1 / x\<^sup>2) *\<^sub>H e2 + (2 / x ^ 3) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> (0::'a) \<Longrightarrow> (*h* inverse) (\<beta> x) = inverse x *\<^sub>H ba - ((1::'a) / x\<^sup>2) *\<^sub>H e1 - ((1::'a) / x\<^sup>2) *\<^sub>H e2 + ((2::'a) / x ^ 3) *\<^sub>H e12
[PROOF STEP]
by (simp add: hypext_extract_eq divide_inverse of_comp_minus scaleH_times)


[STATEMENT]
lemma inverse_extract:
  "x \<noteq> 0 \<Longrightarrow> inverse (\<beta> x) = inverse x *\<^sub>H ba - (1 / x\<^sup>2) *\<^sub>H e1 - (1 / x\<^sup>2) *\<^sub>H e2 + (2 / x ^ 3) *\<^sub>H e12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> (0::'a) \<Longrightarrow> inverse (\<beta> x) = inverse x *\<^sub>H ba - ((1::'a) / x\<^sup>2) *\<^sub>H e1 - ((1::'a) / x\<^sup>2) *\<^sub>H e2 + ((2::'a) / x ^ 3) *\<^sub>H e12
[PROOF STEP]
by (metis hyperdual.sel(1) hyperdualx_def hypext_inverse hypext_inverse_extract)


[STATEMENT]
lemma Eps1_hypext_inverse [simp]:
  "Base x \<noteq> 0 \<Longrightarrow> Eps1 ((*h* inverse) x) = - Eps1 x * (1 / (Base x)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Base x \<noteq> (0::'a) \<Longrightarrow> Eps1 ((*h* inverse) x) = - Eps1 x * ((1::'a) / (Base x)\<^sup>2)
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps1_inverse [simp]:
  "Base (x::'a::real_normed_field hyperdual) \<noteq> 0 \<Longrightarrow> Eps1 (inverse x) = - Eps1 x * (1 / (Base x)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Base x \<noteq> (0::'a) \<Longrightarrow> Eps1 (inverse x) = - Eps1 x * ((1::'a) / (Base x)\<^sup>2)
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps2_hypext_inverse [simp]:
  "Base (x::'a::real_normed_field hyperdual) \<noteq> 0 \<Longrightarrow> Eps2 (inverse x) = - Eps2 x * (1 / (Base x)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Base x \<noteq> (0::'a) \<Longrightarrow> Eps2 (inverse x) = - Eps2 x * ((1::'a) / (Base x)\<^sup>2)
[PROOF STEP]
by simp


[STATEMENT]
lemma Eps12_hypext_inverse [simp]:
  "Base  (x::'a::real_normed_field hyperdual) \<noteq> 0
   \<Longrightarrow> Eps12 (inverse x) = Eps1 x * Eps2 x * (2/ (Base x ^ 3)) - Eps12 x / (Base x)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Base x \<noteq> (0::'a) \<Longrightarrow> Eps12 (inverse x) = Eps1 x * Eps2 x * ((2::'a) / Base x ^ 3) - Eps12 x / (Base x)\<^sup>2
[PROOF STEP]
by simp


[STATEMENT]
lemma hypext_fun_divide:
  assumes "f twice_field_differentiable_at (Base x)"
      and "g twice_field_differentiable_at (Base x)"
      and "g (Base x) \<noteq> 0"
    shows "(*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x
[PROOF STEP]
have "(\<lambda>x. inverse (g x)) twice_field_differentiable_at Base x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. inverse (g x)) twice_field_differentiable_at Base x
[PROOF STEP]
by (simp add: assms(2) assms(3) twice_field_differentiable_at_compose)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. inverse (g x)) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. inverse (g x)) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x
[PROOF STEP]
have "(*h* f) x * (*h* (\<lambda>x. inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* f) x * (*h* (\<lambda>x. inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)
[PROOF STEP]
by (simp add: assms(2) assms(3) hypext_fun_inverse)
[PROOF STATE]
proof (state)
this:
(*h* f) x * (*h* (\<lambda>x. inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. inverse (g x)) twice_field_differentiable_at Base x
(*h* f) x * (*h* (\<lambda>x. inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)
[PROOF STEP]
have "(*h* (\<lambda>x. f x * inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. inverse (g x)) twice_field_differentiable_at Base x
(*h* f) x * (*h* (\<lambda>x. inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. f x * inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)
[PROOF STEP]
by (simp add: assms(1) hypext_fun_mult)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. f x * inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(*h* (\<lambda>x. f x * inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(*h* (\<lambda>x. f x * inverse (g x))) x = (*h* f) x * inverse ((*h* g) x)

goal (1 subgoal):
 1. (*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x
[PROOF STEP]
by (simp add: divide_inverse hyp_divide_inverse)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. f x / g x)) x = (*h* f) x / (*h* g) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hypext_polyn:
  fixes coef :: "nat \<Rightarrow> 'a :: {real_normed_field}"
    and n :: nat
  shows "(*h* (\<lambda>x. \<Sum>i<n. coef i * x^i)) x = (\<Sum>i<n. (coef i) *\<^sub>H (x^i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i)
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (*h* (\<lambda>x. \<Sum>i<0. coef i * x ^ i)) x = (\<Sum>i<0. coef i *\<^sub>H x ^ i)
 2. \<And>n. (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) \<Longrightarrow> (*h* (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i)) x = (\<Sum>i<Suc n. coef i *\<^sub>H x ^ i)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (*h* (\<lambda>x. \<Sum>i<0. coef i * x ^ i)) x = (\<Sum>i<0. coef i *\<^sub>H x ^ i)
 2. \<And>n. (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) \<Longrightarrow> (*h* (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i)) x = (\<Sum>i<Suc n. coef i *\<^sub>H x ^ i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. \<Sum>i<0. coef i * x ^ i)) x = (\<Sum>i<0. coef i *\<^sub>H x ^ i)
[PROOF STEP]
by (simp add: zero_hyperdual_def)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. \<Sum>i<0. coef i * x ^ i)) x = (\<Sum>i<0. coef i *\<^sub>H x ^ i)

goal (1 subgoal):
 1. \<And>n. (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) \<Longrightarrow> (*h* (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i)) x = (\<Sum>i<Suc n. coef i *\<^sub>H x ^ i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) \<Longrightarrow> (*h* (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i)) x = (\<Sum>i<Suc n. coef i *\<^sub>H x ^ i)
[PROOF STEP]
case hyp: (Suc n)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i)

goal (1 subgoal):
 1. \<And>n. (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) \<Longrightarrow> (*h* (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i)) x = (\<Sum>i<Suc n. coef i *\<^sub>H x ^ i)
[PROOF STEP]
have "(\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)"
   and "(\<lambda>x. \<Sum>i<Suc n. coef i *\<^sub>H x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n) &&& (\<lambda>x. \<Sum>i<Suc n. coef i *\<^sub>H x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n)
[PROOF STEP]
by (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)
(\<lambda>x. \<Sum>i<Suc n. coef i *\<^sub>H x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n)

goal (1 subgoal):
 1. \<And>n. (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) \<Longrightarrow> (*h* (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i)) x = (\<Sum>i<Suc n. coef i *\<^sub>H x ^ i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)
(\<lambda>x. \<Sum>i<Suc n. coef i *\<^sub>H x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)
(\<lambda>x. \<Sum>i<Suc n. coef i *\<^sub>H x ^ i) = (\<lambda>x. (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n)

goal (1 subgoal):
 1. (*h* (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i)) x = (\<Sum>i<Suc n. coef i *\<^sub>H x ^ i)
[PROOF STEP]
proof (simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
have "(\<lambda>x. coef n * x ^ n) twice_field_differentiable_at Base x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. coef n * x ^ n) twice_field_differentiable_at Base x
[PROOF STEP]
using twice_field_differentiable_at_compose[of "\<lambda>x. x ^ n" "Base x" "(*) (coef n)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(\<lambda>x. x ^ n) twice_field_differentiable_at Base x; (*) (coef n) twice_field_differentiable_at Base x ^ n\<rbrakk> \<Longrightarrow> (\<lambda>x. coef n * x ^ n) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (\<lambda>x. coef n * x ^ n) twice_field_differentiable_at Base x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. coef n * x ^ n) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. coef n * x ^ n) twice_field_differentiable_at Base x
[PROOF STEP]
have "(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x =
          (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i))) x + (*h* (\<lambda>x. coef n * x ^ n)) x"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. coef n * x ^ n) twice_field_differentiable_at Base x

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x + (*h* (\<lambda>x. coef n * x ^ n)) x
[PROOF STEP]
by (simp add: hypext_fun_add)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x + (*h* (\<lambda>x. coef n * x ^ n)) x

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x + (*h* (\<lambda>x. coef n * x ^ n)) x

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
have "(*h* (\<lambda>x. coef n * x ^ n)) x = coef n *\<^sub>H x ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*h* (\<lambda>x. coef n * x ^ n)) x = coef n *\<^sub>H x ^ n
[PROOF STEP]
by (simp add: hypext_fun_scaleH hypext_power)
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. coef n * x ^ n)) x = coef n *\<^sub>H x ^ n

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x + (*h* (\<lambda>x. coef n * x ^ n)) x
(*h* (\<lambda>x. coef n * x ^ n)) x = coef n *\<^sub>H x ^ n
[PROOF STEP]
have "(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n"
[PROOF STATE]
proof (prove)
using this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x + (*h* (\<lambda>x. coef n * x ^ n)) x
(*h* (\<lambda>x. coef n * x ^ n)) x = coef n *\<^sub>H x ^ n

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
using hyp
[PROOF STATE]
proof (prove)
using this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x + (*h* (\<lambda>x. coef n * x ^ n)) x
(*h* (\<lambda>x. coef n * x ^ n)) x = coef n *\<^sub>H x ^ n
(*h* (\<lambda>x. \<Sum>i<n. coef i * x ^ i)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i)

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
show "(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n"
[PROOF STATE]
proof (prove)
using this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n

goal (1 subgoal):
 1. (*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. (\<Sum>i<n. coef i * x ^ i) + coef n * x ^ n)) x = (\<Sum>i<n. coef i *\<^sub>H x ^ i) + coef n *\<^sub>H x ^ n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(*h* (\<lambda>x. \<Sum>i<Suc n. coef i * x ^ i)) x = (\<Sum>i<Suc n. coef i *\<^sub>H x ^ i)

goal:
No subgoals!
[PROOF STEP]
qed