[STATEMENT]
lemma sets_distinct5: "(s::int) < g \<Longrightarrow> {(a::int, b::int). a = s} \<noteq> {(a::int, b::int).  g < a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < g \<Longrightarrow> {(a, b). a = s} \<noteq> {(a, b). g < a}
[PROOF STEP]
apply (auto simp: sets_distinct3)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "(s,4) \<in> {(a::int,b::int). a = (s)}")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}; (s, 4) \<in> {(a, b). a = s}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}\<rbrakk> \<Longrightarrow> (s, 4) \<in> {(a, b). a = s}
[PROOF STEP]
apply (subgoal_tac "(s,4) \<notin> {(a::int,b::int). g < a}")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}; (s, 4) \<in> {(a, b). a = s}; (s, 4) \<notin> {(a, b). g < a}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}; (s, 4) \<in> {(a, b). a = s}\<rbrakk> \<Longrightarrow> (s, 4) \<notin> {(a, b). g < a}
 3. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}\<rbrakk> \<Longrightarrow> (s, 4) \<in> {(a, b). a = s}
[PROOF STEP]
apply (erule aux)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}; (s, 4) \<notin> {(a, b). g < a}\<rbrakk> \<Longrightarrow> (s, 4) \<notin> ?d5
 2. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}; (s, 4) \<notin> {(a, b). g < a}\<rbrakk> \<Longrightarrow> {(a, b). a = s} = ?d5
 3. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}; (s, 4) \<in> {(a, b). a = s}\<rbrakk> \<Longrightarrow> (s, 4) \<notin> {(a, b). g < a}
 4. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}\<rbrakk> \<Longrightarrow> (s, 4) \<in> {(a, b). a = s}
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}; (s, 4) \<in> {(a, b). a = s}\<rbrakk> \<Longrightarrow> (s, 4) \<notin> {(a, b). g < a}
 2. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}\<rbrakk> \<Longrightarrow> (s, 4) \<in> {(a, b). a = s}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s < g; {(a, b). a = s} = {(a, b). g < a}\<rbrakk> \<Longrightarrow> (s, 4) \<in> {(a, b). a = s}
[PROOF STEP]
by blast


[STATEMENT]
lemma sets_distinct6: "(s::int) < g \<Longrightarrow> {(a::int, b::int).  g < a} \<noteq> {(a::int, b::int).  a = s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < g \<Longrightarrow> {(a, b). g < a} \<noteq> {(a, b). a = s}
[PROOF STEP]
apply (rule not_sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < g \<Longrightarrow> {(a, b). a = s} \<noteq> {(a, b). g < a}
[PROOF STEP]
apply (rule sets_distinct5)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < g \<Longrightarrow> s < g
[PROOF STEP]
by simp


[STATEMENT]
lemma distinctNets: "FWLink \<noteq>  any \<and> FWLink \<noteq>  i4 \<and> FWLink \<noteq>  i27 \<and> FWLink \<noteq>  eth_intern \<and> FWLink \<noteq>   eth_private \<and>
any \<noteq>  FWLink \<and> any \<noteq>  i4 \<and> any \<noteq>  i27 \<and> any \<noteq>  eth_intern \<and> any \<noteq>  eth_private \<and> i4 \<noteq>  FWLink \<and>
i4 \<noteq>  any \<and> i4 \<noteq>  i27 \<and> i4 \<noteq>  eth_intern \<and> i4 \<noteq>  eth_private \<and> i27 \<noteq>  FWLink \<and> i27 \<noteq>  any \<and>
i27 \<noteq>  i4 \<and> i27 \<noteq>  eth_intern \<and> i27 \<noteq>  eth_private \<and> eth_intern \<noteq>  FWLink \<and> eth_intern \<noteq>  any \<and>
eth_intern \<noteq>  i4 \<and> eth_intern \<noteq>  i27 \<and> eth_intern \<noteq>  eth_private \<and> eth_private \<noteq>  FWLink \<and>
eth_private \<noteq>  any \<and> eth_private \<noteq>  i4 \<and> eth_private \<noteq>  i27 \<and> eth_private \<noteq>  eth_intern"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWLink \<noteq> any \<and> FWLink \<noteq> i4 \<and> FWLink \<noteq> i27 \<and> FWLink \<noteq> eth_intern \<and> FWLink \<noteq> eth_private \<and> any \<noteq> FWLink \<and> any \<noteq> i4 \<and> any \<noteq> i27 \<and> any \<noteq> eth_intern \<and> any \<noteq> eth_private \<and> i4 \<noteq> FWLink \<and> i4 \<noteq> any \<and> i4 \<noteq> i27 \<and> i4 \<noteq> eth_intern \<and> i4 \<noteq> eth_private \<and> i27 \<noteq> FWLink \<and> i27 \<noteq> any \<and> i27 \<noteq> i4 \<and> i27 \<noteq> eth_intern \<and> i27 \<noteq> eth_private \<and> eth_intern \<noteq> FWLink \<and> eth_intern \<noteq> any \<and> eth_intern \<noteq> i4 \<and> eth_intern \<noteq> i27 \<and> eth_intern \<noteq> eth_private \<and> eth_private \<noteq> FWLink \<and> eth_private \<noteq> any \<and> eth_private \<noteq> i4 \<and> eth_private \<noteq> i27 \<and> eth_private \<noteq> eth_intern
[PROOF STEP]
by (simp add: PolicyLemmas sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4
                sets_distinct5 sets_distinct6)


[STATEMENT]
lemma aux5: "\<lbrakk>x \<noteq> a; y\<noteq>b; (x \<noteq> y \<and> x \<noteq> b) \<or>  (a \<noteq> b \<and> a \<noteq> y)\<rbrakk> \<Longrightarrow> {x,a} \<noteq> {y,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> a; y \<noteq> b; x \<noteq> y \<and> x \<noteq> b \<or> a \<noteq> b \<and> a \<noteq> y\<rbrakk> \<Longrightarrow> {x, a} \<noteq> {y, b}
[PROOF STEP]
by auto


[STATEMENT]
lemma aux2: "{a,b} = {b,a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a, b} = {b, a}
[PROOF STEP]
by auto


[STATEMENT]
lemma ANDex: "allNetsDistinct (policy2list Policy)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. allNetsDistinct (policy2list Policy)
[PROOF STEP]
apply (simp add: PolicyL allNetsDistinct_def distinctNets)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. a \<noteq> b \<and> (a = i4 \<or> a = FWLink \<or> a = i27 \<or> a = any) \<and> (b = i4 \<or> b = FWLink \<or> b = i27 \<or> b = any) \<longrightarrow> netsDistinct a b
[PROOF STEP]
by (auto simp: PLemmas PolicyLemmas netsDistinct_def sets_distinct5 sets_distinct6)


[STATEMENT]
lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_in_list (policy2list Policy) (Nets_List Policy)
[PROOF STEP]
apply (simp add: PolicyL)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {FWLink, i4} \<in> set (Nets_List (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) \<and> {FWLink} \<in> set (Nets_List (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) \<and> {any, FWLink} \<in> set (Nets_List (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) \<and> {i27, any} \<in> set (Nets_List (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) \<and> {any} \<in> set (Nets_List (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))
[PROOF STEP]
apply (unfold Nets_List_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {FWLink, i4} \<in> set (makeSets (normBothNets (bothNets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)))) \<and> {FWLink} \<in> set (makeSets (normBothNets (bothNets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)))) \<and> {any, FWLink} \<in> set (makeSets (normBothNets (bothNets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)))) \<and> {i27, any} \<in> set (makeSets (normBothNets (bothNets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)))) \<and> {any} \<in> set (makeSets (normBothNets (bothNets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))
[PROOF STEP]
apply (unfold bothNets_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {FWLink, i4} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))) \<and> {FWLink} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))) \<and> {any, FWLink} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))) \<and> {i27, any} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))) \<and> {any} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)))))
[PROOF STEP]
apply (insert distinctNets)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWLink \<noteq> any \<and> FWLink \<noteq> i4 \<and> FWLink \<noteq> i27 \<and> FWLink \<noteq> eth_intern \<and> FWLink \<noteq> eth_private \<and> any \<noteq> FWLink \<and> any \<noteq> i4 \<and> any \<noteq> i27 \<and> any \<noteq> eth_intern \<and> any \<noteq> eth_private \<and> i4 \<noteq> FWLink \<and> i4 \<noteq> any \<and> i4 \<noteq> i27 \<and> i4 \<noteq> eth_intern \<and> i4 \<noteq> eth_private \<and> i27 \<noteq> FWLink \<and> i27 \<noteq> any \<and> i27 \<noteq> i4 \<and> i27 \<noteq> eth_intern \<and> i27 \<noteq> eth_private \<and> eth_intern \<noteq> FWLink \<and> eth_intern \<noteq> any \<and> eth_intern \<noteq> i4 \<and> eth_intern \<noteq> i27 \<and> eth_intern \<noteq> eth_private \<and> eth_private \<noteq> FWLink \<and> eth_private \<noteq> any \<and> eth_private \<noteq> i4 \<and> eth_private \<noteq> i27 \<and> eth_private \<noteq> eth_intern \<Longrightarrow> {FWLink, i4} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))) \<and> {FWLink} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))) \<and> {any, FWLink} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))) \<and> {i27, any} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7))))) \<and> {any} \<in> set (makeSets (normBothNets (zip (srcnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)) (destnets (DenyAll \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> (AllowPortFromTo FWLink i4 6 \<oplus> AllowPortFromTo FWLink i4 7) \<oplus> AllowPortFromTo FWLink FWLink 4 \<oplus> AllowPortFromTo any FWLink 1 \<oplus> (AllowPortFromTo i27 any 1 \<oplus> AllowPortFromTo i27 any 2 \<oplus> AllowPortFromTo i27 any 3) \<oplus> AllowPortFromTo any any 7)))))
[PROOF STEP]
by simp


[STATEMENT]
lemma [sep_heap_rules]: "< emp > arl_empty <is_array_list []>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> arl_empty <is_array_list []>
[PROOF STEP]
by (sep_auto simp: arl_empty_def is_array_list_def initial_capacity_def)


[STATEMENT]
lemma [sep_heap_rules]: "i<length l \<Longrightarrow> < is_array_list l a > arl_nth a i <\<lambda>x. is_array_list l a * \<up>(x = l!i) >"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length l \<Longrightarrow> <is_array_list l a> arl_nth a i <\<lambda>x. is_array_list l a * \<up> (x = l ! i)>
[PROOF STEP]
by (sep_auto simp: arl_nth_def is_array_list_def split: prod.splits)


[STATEMENT]
lemma [sep_heap_rules]: "
    < is_array_list l a >
      arl_append a x
    <\<lambda>a. is_array_list (l@[x]) a >\<^sub>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <is_array_list l a> arl_append a x <is_array_list (l @ [x])>\<^sub>t
[PROOF STEP]
by (sep_auto
      simp: arl_append_def is_array_list_def take_update_last neq_Nil_conv
      split: prod.splits nat.split)


[STATEMENT]
lemma is_array_list_prec: "precise is_array_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise is_array_list
[PROOF STEP]
unfolding is_array_list_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise (\<lambda>l (a, n). \<exists>\<^sub>Al'. a \<mapsto>\<^sub>a l' * \<up> (n \<le> length l' \<and> l = take n l' \<and> 0 < length l'))
[PROOF STEP]
apply(rule preciseI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> (case p of (aa, n) \<Rightarrow> \<exists>\<^sub>Al'. aa \<mapsto>\<^sub>a l' * \<up> (n \<le> length l' \<and> a = take n l' \<and> 0 < length l')) * F \<and>\<^sub>A (case p of (a, n) \<Rightarrow> \<exists>\<^sub>Al'. a \<mapsto>\<^sub>a l' * \<up> (n \<le> length l' \<and> a' = take n l' \<and> 0 < length l')) * F' \<Longrightarrow> a = a'
[PROOF STEP]
apply(simp split: prod.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F' x1 x2. \<lbrakk>p = (x1, x2); \<exists>l' l'a. h \<Turnstile> x1 \<mapsto>\<^sub>a l'a * F \<and>\<^sub>A x1 \<mapsto>\<^sub>a l' * F' \<and> x2 \<le> length l'a \<and> a = take x2 l'a \<and> l'a \<noteq> [] \<and> x2 \<le> length l' \<and> a' = take x2 l' \<and> l' \<noteq> []\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
using preciseD snga_prec
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>precise ?R; ?h \<Turnstile> ?R ?a ?p * ?F \<and>\<^sub>A ?R ?a' ?p * ?F'\<rbrakk> \<Longrightarrow> ?a = ?a'
precise (\<lambda>x p. p \<mapsto>\<^sub>a x)

goal (1 subgoal):
 1. \<And>a a' h p F F' x1 x2. \<lbrakk>p = (x1, x2); \<exists>l' l'a. h \<Turnstile> x1 \<mapsto>\<^sub>a l'a * F \<and>\<^sub>A x1 \<mapsto>\<^sub>a l' * F' \<and> x2 \<le> length l'a \<and> a = take x2 l'a \<and> l'a \<noteq> [] \<and> x2 \<le> length l' \<and> a' = take x2 l' \<and> l' \<noteq> []\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
by fastforce


[STATEMENT]
lemma is_array_list_lengthIA: "is_array_list l li \<Longrightarrow>\<^sub>A \<up>(snd li = length l) * true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_array_list l li \<Longrightarrow>\<^sub>A \<up> (snd li = length l) * true
[PROOF STEP]
by(sep_auto simp: is_array_list_def split: prod.splits)


[STATEMENT]
lemma is_array_list_lengthI: "x \<Turnstile> is_array_list l li \<Longrightarrow> snd li = length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<Turnstile> is_array_list l li \<Longrightarrow> snd li = length l
[PROOF STEP]
using is_array_list_lengthIA
[PROOF STATE]
proof (prove)
using this:
is_array_list ?l ?li \<Longrightarrow>\<^sub>A \<up> (snd ?li = length ?l) * true

goal (1 subgoal):
 1. x \<Turnstile> is_array_list l li \<Longrightarrow> snd li = length l
[PROOF STEP]
by (metis (full_types) ent_pure_post_iff star_aci(2))


[STATEMENT]
lemma  phl_n_while:
  assumes "\<lbrace>n x \<cdot>  n y\<rbrace> z \<lbrace>n x\<rbrace>"
  shows "\<lbrace>n x\<rbrace> (n y \<cdot> z)\<^sup>\<infinity> \<cdot> t y \<lbrace>n x \<cdot> t y\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>!x\<rparr>(!y \<cdot> z)\<^sup>\<infinity> \<cdot> t y\<lparr>(!y \<cdot> z)\<^sup>\<infinity> \<cdot> t y \<cdot> (!x \<cdot> t y)\<rparr>
[PROOF STEP]
by (metis assms phl.ht_at_phl_while t_n_closed)


[STATEMENT]
lemma phl_test_while:
  assumes "test p" and "test b"
  and "\<lbrace>p \<cdot> b\<rbrace> x \<lbrace>p\<rbrace>"
  shows "\<lbrace>p\<rbrace> (b \<cdot> x)\<^sup>\<infinity> \<cdot> !b \<lbrace>p \<cdot> !b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>p\<rparr>while b do x od\<lparr>(while b do x od) \<cdot> (p \<cdot> !b)\<rparr>
[PROOF STEP]
by (metis assms phl_n_while test_double_comp_var)


[STATEMENT]
lemma phl_while_syntax:
  assumes "test p" and "test b" and "\<lbrace>p \<cdot> b\<rbrace> x \<lbrace>p\<rbrace>"
  shows "\<lbrace>p\<rbrace> while b do x od \<lbrace>p \<cdot> !b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>p\<rparr>while b do x od\<lparr>(while b do x od) \<cdot> (p \<cdot> !b)\<rparr>
[PROOF STEP]
by (metis assms phl_test_while)


[STATEMENT]
lemma fact_dvd_pochhammer:
  assumes "m \<le> n + 1"
  shows   "fact m dvd pochhammer (int n - int m + 1) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact m dvd pochhammer (int n - int m + 1) m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fact m dvd pochhammer (int n - int m + 1) m
[PROOF STEP]
have "(real n gchoose m) * fact m = of_int (pochhammer (int n - int m + 1) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real n gchoose m) * fact m = real_of_int (pochhammer (int n - int m + 1) m)
[PROOF STEP]
by (simp add: gbinomial_pochhammer' pochhammer_of_int [symmetric])
[PROOF STATE]
proof (state)
this:
(real n gchoose m) * fact m = real_of_int (pochhammer (int n - int m + 1) m)

goal (1 subgoal):
 1. fact m dvd pochhammer (int n - int m + 1) m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(real n gchoose m) * fact m = real_of_int (pochhammer (int n - int m + 1) m)

goal (1 subgoal):
 1. fact m dvd pochhammer (int n - int m + 1) m
[PROOF STEP]
have "(real n gchoose m) * fact m = of_int (int (n choose m) * fact m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real n gchoose m) * fact m = real_of_int (int (n choose m) * fact m)
[PROOF STEP]
by (simp add: binomial_gbinomial)
[PROOF STATE]
proof (state)
this:
(real n gchoose m) * fact m = real_of_int (int (n choose m) * fact m)

goal (1 subgoal):
 1. fact m dvd pochhammer (int n - int m + 1) m
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int (int (n choose m) * fact m) = real_of_int (pochhammer (int n - int m + 1) m)
[PROOF STEP]
have "int (n choose m) * fact m = pochhammer (int n - int m + 1) m"
[PROOF STATE]
proof (prove)
using this:
real_of_int (int (n choose m) * fact m) = real_of_int (pochhammer (int n - int m + 1) m)

goal (1 subgoal):
 1. int (n choose m) * fact m = pochhammer (int n - int m + 1) m
[PROOF STEP]
by (subst (asm) of_int_eq_iff)
[PROOF STATE]
proof (state)
this:
int (n choose m) * fact m = pochhammer (int n - int m + 1) m

goal (1 subgoal):
 1. fact m dvd pochhammer (int n - int m + 1) m
[PROOF STEP]
from this [symmetric]
[PROOF STATE]
proof (chain)
picking this:
pochhammer (int n - int m + 1) m = int (n choose m) * fact m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pochhammer (int n - int m + 1) m = int (n choose m) * fact m

goal (1 subgoal):
 1. fact m dvd pochhammer (int n - int m + 1) m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fact m dvd pochhammer (int n - int m + 1) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_nat_eq_1_iff [simp]: "of_nat x = (1 :: 'a :: semiring_char_0) \<longleftrightarrow> x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_nat x = (1::'a)) = (x = 1)
[PROOF STEP]
by (fact of_nat_eq_1_iff)


[STATEMENT]
lemma prime_elem_int_not_dvd_neg1_power:
  "prime_elem (p :: int) \<Longrightarrow> \<not>p dvd (-1) ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem p \<Longrightarrow> \<not> p dvd (- 1) ^ n
[PROOF STEP]
by (rule notI, frule (1) prime_elem_dvd_power, cases "p \<ge> 0") (auto simp: prime_elem_def)


[STATEMENT]
lemma nat_fact [simp]: "nat (fact n) = fact n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (fact n) = fact n
[PROOF STEP]
by (subst of_nat_fact [symmetric]) (rule nat_int)


[STATEMENT]
lemma prime_dvd_fact_iff_int:
  "p dvd fact n \<longleftrightarrow> p \<le> int n" if "prime p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p dvd fact n) = (p \<le> int n)
[PROOF STEP]
using that prime_dvd_fact_iff [of "nat \<bar>p\<bar>" n]
[PROOF STATE]
proof (prove)
using this:
prime p
prime (nat \<bar>p\<bar>) \<Longrightarrow> (nat \<bar>p\<bar> dvd fact n) = (nat \<bar>p\<bar> \<le> n)

goal (1 subgoal):
 1. (p dvd fact n) = (p \<le> int n)
[PROOF STEP]
by auto (simp add: prime_ge_0_int)


[STATEMENT]
lemma filterlim_minus_nat_at_top:
  "filterlim (\<lambda>n. n - k :: nat) at_top at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM n sequentially. n - k :> sequentially
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LIM n sequentially. n - k :> sequentially
[PROOF STEP]
have "sequentially = filtermap (\<lambda>n. n + k) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sequentially = filtermap (\<lambda>n. n + k) sequentially
[PROOF STEP]
by (auto simp: filter_eq_iff eventually_filtermap)
[PROOF STATE]
proof (state)
this:
sequentially = filtermap (\<lambda>n. n + k) sequentially

goal (1 subgoal):
 1. LIM n sequentially. n - k :> sequentially
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sequentially = filtermap (\<lambda>n. n + k) sequentially

goal (1 subgoal):
 1. LIM n sequentially. n - k :> sequentially
[PROOF STEP]
have "filterlim (\<lambda>n. n - k :: nat) at_top \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM n filtermap (\<lambda>n. n + k) sequentially. n - k :> sequentially
[PROOF STEP]
by (simp add: filterlim_filtermap filterlim_ident)
[PROOF STATE]
proof (state)
this:
LIM n filtermap (\<lambda>n. n + k) sequentially. n - k :> sequentially

goal (1 subgoal):
 1. LIM n sequentially. n - k :> sequentially
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
LIM n sequentially. n - k :> sequentially
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
LIM n sequentially. n - k :> sequentially

goal (1 subgoal):
 1. LIM n sequentially. n - k :> sequentially
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
LIM n sequentially. n - k :> sequentially

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_over_fact_tendsto_0:
  "(\<lambda>n. (x :: real) ^ n / fact n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. x ^ n / fact n) \<longlonglongrightarrow> 0
[PROOF STEP]
using summable_exp[of x]
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. inverse (fact n) * x ^ n)

goal (1 subgoal):
 1. (\<lambda>n. x ^ n / fact n) \<longlonglongrightarrow> 0
[PROOF STEP]
by (intro summable_LIMSEQ_zero) (simp add: sums_iff field_simps)


[STATEMENT]
lemma power_over_fact_tendsto_0':
  "(\<lambda>n. c * (x :: real) ^ n / fact n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. c * x ^ n / fact n) \<longlonglongrightarrow> 0
[PROOF STEP]
using tendsto_mult[OF tendsto_const[of c] power_over_fact_tendsto_0[of x]]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>xa. c * (x ^ xa / fact xa)) \<longlonglongrightarrow> c * 0

goal (1 subgoal):
 1. (\<lambda>n. c * x ^ n / fact n) \<longlonglongrightarrow> 0
[PROOF STEP]
by simp


[STATEMENT]
lemma of_int_poly_0 [simp]: "of_int_poly 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly 0 = 0
[PROOF STEP]
by transfer (simp add: fun_eq_iff)


[STATEMENT]
lemma of_int_poly_pCons [simp]: "of_int_poly (pCons c p) = pCons (of_int c) (of_int_poly p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (pCons c p) = pCons (of_int c) (of_int_poly p)
[PROOF STEP]
by transfer' (simp add: fun_eq_iff split: nat.splits)


[STATEMENT]
lemma of_int_poly_smult [simp]: "of_int_poly (smult c p) = smult (of_int c) (of_int_poly p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (Polynomial.smult c p) = Polynomial.smult (of_int c) (of_int_poly p)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma of_int_poly_1 [simp]: "of_int_poly 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly 1 = 1
[PROOF STEP]
by (simp add: one_pCons)


[STATEMENT]
lemma of_int_poly_add [simp]: "of_int_poly (p + q) = of_int_poly p + of_int_poly q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (p + q) = of_int_poly p + of_int_poly q
[PROOF STEP]
by transfer' (simp add: fun_eq_iff)


[STATEMENT]
lemma of_int_poly_mult [simp]: "of_int_poly (p * q) = (of_int_poly p * of_int_poly q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (p * q) = of_int_poly p * of_int_poly q
[PROOF STEP]
by (induction p) simp_all


[STATEMENT]
lemma of_int_poly_sum [simp]: "of_int_poly (sum f A) = sum (\<lambda>x. of_int_poly (f x)) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (sum f A) = (\<Sum>x\<in>A. of_int_poly (f x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) simp_all


[STATEMENT]
lemma of_int_poly_prod [simp]: "of_int_poly (prod f A) = prod (\<lambda>x. of_int_poly (f x)) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (prod f A) = (\<Prod>x\<in>A. of_int_poly (f x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) simp_all


[STATEMENT]
lemma of_int_poly_power [simp]: "of_int_poly (p ^ n) = of_int_poly p ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (p ^ n) = of_int_poly p ^ n
[PROOF STEP]
by (induction n) simp_all


[STATEMENT]
lemma of_int_poly_monom [simp]: "of_int_poly (monom c n) = monom (of_int c) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly (Polynomial.monom c n) = Polynomial.monom (of_int c) n
[PROOF STEP]
by transfer (simp add: fun_eq_iff)


[STATEMENT]
lemma poly_of_int_poly [simp]: "poly (of_int_poly p) (of_int x) = of_int (poly p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly p) (of_int x) = of_int (poly p x)
[PROOF STEP]
by (induction p) simp_all


[STATEMENT]
lemma poly_of_int_poly_of_nat [simp]: "poly (of_int_poly p) (of_nat x) = of_int (poly p (int x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly p) (of_nat x) = of_int (poly p (int x))
[PROOF STEP]
by (induction p) simp_all


[STATEMENT]
lemma poly_of_int_poly_0 [simp]: "poly (of_int_poly p) 0 = of_int (poly p 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly p) (0::'a) = of_int (poly p 0)
[PROOF STEP]
by (induction p) simp_all


[STATEMENT]
lemma poly_of_int_poly_1 [simp]: "poly (of_int_poly p) 1 = of_int (poly p 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly p) (1::'a) = of_int (poly p 1)
[PROOF STEP]
by (induction p) simp_all


[STATEMENT]
lemma poly_of_int_poly_of_real [simp]:
    "poly (of_int_poly p) (of_real x) = of_real (poly (of_int_poly p) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (of_int_poly p) (of_real x) = of_real (poly (of_int_poly p) x)
[PROOF STEP]
by (induction p) simp_all


[STATEMENT]
lemma of_int_poly_eq_iff [simp]:
  "of_int_poly p = (of_int_poly q :: 'a :: {comm_ring_1, ring_char_0} poly) \<longleftrightarrow> p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_poly p = of_int_poly q) = (p = q)
[PROOF STEP]
by (simp add: poly_eq_iff)


[STATEMENT]
lemma of_int_poly_eq_0_iff [simp]:
  "of_int_poly p = (0 :: 'a :: {comm_ring_1, ring_char_0} poly) \<longleftrightarrow> p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int_poly p = 0) = (p = 0)
[PROOF STEP]
using of_int_poly_eq_iff[of p 0]
[PROOF STATE]
proof (prove)
using this:
(of_int_poly p = of_int_poly 0) = (p = 0)

goal (1 subgoal):
 1. (of_int_poly p = 0) = (p = 0)
[PROOF STEP]
by (simp del: of_int_poly_eq_iff)


[STATEMENT]
lemma degree_of_int_poly [simp]:
  "degree (of_int_poly p :: 'a :: {comm_ring_1, ring_char_0} poly) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (of_int_poly p) = degree p
[PROOF STEP]
by (simp add: degree_def)


[STATEMENT]
lemma pderiv_of_int_poly [simp]: "pderiv (of_int_poly p) = of_int_poly (pderiv p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv (of_int_poly p) = of_int_poly (pderiv p)
[PROOF STEP]
by (induction p) (simp_all add: pderiv_pCons)


[STATEMENT]
lemma higher_pderiv_of_int_poly [simp]:
  "(pderiv ^^ n) (of_int_poly p) = of_int_poly ((pderiv ^^ n) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pderiv ^^ n) (of_int_poly p) = of_int_poly ((pderiv ^^ n) p)
[PROOF STEP]
by (induction n) simp_all


[STATEMENT]
lemma int_polyE:
  assumes "\<And>n. coeff (p :: 'a :: {comm_ring_1, ring_char_0} poly) n \<in> \<int>"
  obtains p' where "p = of_int_poly p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p'. p = of_int_poly p' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p'. p = of_int_poly p' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
poly.coeff p ?n \<in> \<int>
[PROOF STEP]
have "\<forall>n. \<exists>c. coeff p n = of_int c"
[PROOF STATE]
proof (prove)
using this:
poly.coeff p ?n \<in> \<int>

goal (1 subgoal):
 1. \<forall>n. \<exists>c. poly.coeff p n = of_int c
[PROOF STEP]
by (auto simp: Ints_def)
[PROOF STATE]
proof (state)
this:
\<forall>n. \<exists>c. poly.coeff p n = of_int c

goal (1 subgoal):
 1. (\<And>p'. p = of_int_poly p' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "\<exists>c. \<forall>n. of_int (c n) = coeff p n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<exists>c. poly.coeff p n = of_int c

goal (1 subgoal):
 1. \<exists>c. \<forall>n. of_int (c n) = poly.coeff p n
[PROOF STEP]
by (simp add: choice_iff eq_commute)
[PROOF STATE]
proof (state)
this:
\<exists>c. \<forall>n. of_int (c n) = poly.coeff p n

goal (1 subgoal):
 1. (\<And>p'. p = of_int_poly p' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. \<forall>n. of_int (c n) = poly.coeff p n
[PROOF STEP]
obtain c where c: "of_int (c n) = coeff p n" for n
[PROOF STATE]
proof (prove)
using this:
\<exists>c. \<forall>n. of_int (c n) = poly.coeff p n

goal (1 subgoal):
 1. (\<And>c. (\<And>n. of_int (c n) = poly.coeff p n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
of_int (c ?n) = poly.coeff p ?n

goal (1 subgoal):
 1. (\<And>p'. p = of_int_poly p' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have [simp]: "coeff (Abs_poly c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff (Abs_poly c) = c
[PROOF STEP]
proof (rule poly.Abs_poly_inverse, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>n. c n = 0
[PROOF STEP]
have "eventually (\<lambda>n. n > degree p) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eventually ((<) (degree p)) sequentially
[PROOF STEP]
by (rule eventually_gt_at_top)
[PROOF STATE]
proof (state)
this:
eventually ((<) (degree p)) sequentially

goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>n. c n = 0
[PROOF STEP]
hence "eventually (\<lambda>n. coeff p n = 0) at_top"
[PROOF STATE]
proof (prove)
using this:
eventually ((<) (degree p)) sequentially

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. poly.coeff p n = (0::'a)
[PROOF STEP]
by eventually_elim (simp add: coeff_eq_0)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. poly.coeff p n = (0::'a)

goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>n. c n = 0
[PROOF STEP]
thus "eventually (\<lambda>n. c n = 0) cofinite"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. poly.coeff p n = (0::'a)

goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>n. c n = 0
[PROOF STEP]
by (simp add: c [symmetric] cofinite_eq_sequentially)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>\<infinity>n. c n = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly.coeff (Abs_poly c) = c

goal (1 subgoal):
 1. (\<And>p'. p = of_int_poly p' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "p = of_int_poly (Abs_poly c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = of_int_poly (Abs_poly c)
[PROOF STEP]
by (rule poly_eqI) (simp add: c)
[PROOF STATE]
proof (state)
this:
p = of_int_poly (Abs_poly c)

goal (1 subgoal):
 1. (\<And>p'. p = of_int_poly p' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = of_int_poly (Abs_poly c)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pderiv_power:
  "pderiv (p ^ n) = smult (of_nat n) (p ^ (n - 1) * pderiv p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv (p ^ n) = Polynomial.smult (of_nat n) (p ^ (n - 1) * pderiv p)
[PROOF STEP]
by (cases n) (simp_all add: pderiv_power_Suc del: power_Suc)


[STATEMENT]
lemma degree_prod_sum_eq:
  "(\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0) \<Longrightarrow>
     degree (prod f A :: 'a :: idom poly) = (\<Sum>x\<in>A. degree (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0) \<Longrightarrow> degree (prod f A) = (\<Sum>x\<in>A. degree (f x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq)


[STATEMENT]
lemma pderiv_monom:
  "pderiv (monom c n) = monom (of_nat n * c) (n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pderiv (Polynomial.monom c n) = Polynomial.monom (of_nat n * c) (n - 1)
[PROOF STEP]
by (cases n)
     (simp_all add: monom_altdef pderiv_power_Suc pderiv_smult pderiv_pCons mult_ac del: power_Suc)


[STATEMENT]
lemma power_poly_const [simp]: "[:c:] ^ n = [:c ^ n:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:c:] ^ n = [:c ^ n:]
[PROOF STEP]
by (induction n) (simp_all add: power_commutes)


[STATEMENT]
lemma monom_power: "monom c n ^ k = monom (c ^ k) (n * k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.monom c n ^ k = Polynomial.monom (c ^ k) (n * k)
[PROOF STEP]
by (induction k) (simp_all add: mult_monom)


[STATEMENT]
lemma coeff_higher_pderiv:
  "coeff ((pderiv ^^ m) f) n = pochhammer (of_nat (Suc n)) m * coeff f (n + m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff ((pderiv ^^ m) f) n = pochhammer (of_nat (Suc n)) m * poly.coeff f (n + m)
[PROOF STEP]
by (induction m arbitrary: n) (simp_all add: coeff_pderiv pochhammer_rec algebra_simps)


[STATEMENT]
lemma higher_pderiv_add: "(pderiv ^^ n) (p + q) = (pderiv ^^ n) p + (pderiv ^^ n) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pderiv ^^ n) (p + q) = (pderiv ^^ n) p + (pderiv ^^ n) q
[PROOF STEP]
by (induction n arbitrary: p q) (simp_all del: funpow.simps add: funpow_Suc_right pderiv_add)


[STATEMENT]
lemma higher_pderiv_smult: "(pderiv ^^ n) (smult c p) = smult c ((pderiv ^^ n) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pderiv ^^ n) (Polynomial.smult c p) = Polynomial.smult c ((pderiv ^^ n) p)
[PROOF STEP]
by (induction n arbitrary: p) (simp_all del: funpow.simps add: funpow_Suc_right pderiv_smult)


[STATEMENT]
lemma higher_pderiv_0 [simp]: "(pderiv ^^ n) 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pderiv ^^ n) 0 = 0
[PROOF STEP]
by (induction n) simp_all


[STATEMENT]
lemma higher_pderiv_monom:
  "m \<le> n + 1 \<Longrightarrow> (pderiv ^^ m) (monom c n) = monom (pochhammer (int n - int m + 1) m * c) (n - m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n + 1 \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int m + 1) m * c) (n - m)
[PROOF STEP]
proof (induction m arbitrary: c n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c n. 0 \<le> n + 1 \<Longrightarrow> (pderiv ^^ 0) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int 0 + 1) 0 * c) (n - 0)
 2. \<And>m c n. \<lbrakk>\<And>c n. m \<le> n + 1 \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int m + 1) m * c) (n - m); Suc m \<le> n + 1\<rbrakk> \<Longrightarrow> (pderiv ^^ Suc m) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int (Suc m) + 1) (Suc m) * c) (n - Suc m)
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
m \<le> ?n + 1 \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom ?c ?n) = Polynomial.monom (pochhammer (int ?n - int m + 1) m * ?c) (?n - m)
Suc m \<le> n + 1

goal (2 subgoals):
 1. \<And>c n. 0 \<le> n + 1 \<Longrightarrow> (pderiv ^^ 0) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int 0 + 1) 0 * c) (n - 0)
 2. \<And>m c n. \<lbrakk>\<And>c n. m \<le> n + 1 \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int m + 1) m * c) (n - m); Suc m \<le> n + 1\<rbrakk> \<Longrightarrow> (pderiv ^^ Suc m) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int (Suc m) + 1) (Suc m) * c) (n - Suc m)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
m \<le> ?n + 1 \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom ?c ?n) = Polynomial.monom (pochhammer (int ?n - int m + 1) m * ?c) (?n - m)
Suc m \<le> n + 1

goal (1 subgoal):
 1. (pderiv ^^ Suc m) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int (Suc m) + 1) (Suc m) * c) (n - Suc m)
[PROOF STEP]
by (cases n)
       (simp_all del: funpow.simps add: funpow_Suc_right pderiv_monom pochhammer_rec' Suc.IH)
[PROOF STATE]
proof (state)
this:
(pderiv ^^ Suc m) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int (Suc m) + 1) (Suc m) * c) (n - Suc m)

goal (1 subgoal):
 1. \<And>c n. 0 \<le> n + 1 \<Longrightarrow> (pderiv ^^ 0) (Polynomial.monom c n) = Polynomial.monom (pochhammer (int n - int 0 + 1) 0 * c) (n - 0)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma higher_pderiv_monom_eq_zero:
  "m > n + 1 \<Longrightarrow> (pderiv ^^ m) (monom c n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n + 1 < m \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom c n) = 0
[PROOF STEP]
proof (induction m arbitrary: c n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c n. n + 1 < 0 \<Longrightarrow> (pderiv ^^ 0) (Polynomial.monom c n) = 0
 2. \<And>m c n. \<lbrakk>\<And>c n. n + 1 < m \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom c n) = 0; n + 1 < Suc m\<rbrakk> \<Longrightarrow> (pderiv ^^ Suc m) (Polynomial.monom c n) = 0
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
?n + 1 < m \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom ?c ?n) = 0
n + 1 < Suc m

goal (2 subgoals):
 1. \<And>c n. n + 1 < 0 \<Longrightarrow> (pderiv ^^ 0) (Polynomial.monom c n) = 0
 2. \<And>m c n. \<lbrakk>\<And>c n. n + 1 < m \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom c n) = 0; n + 1 < Suc m\<rbrakk> \<Longrightarrow> (pderiv ^^ Suc m) (Polynomial.monom c n) = 0
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?n + 1 < m \<Longrightarrow> (pderiv ^^ m) (Polynomial.monom ?c ?n) = 0
n + 1 < Suc m

goal (1 subgoal):
 1. (pderiv ^^ Suc m) (Polynomial.monom c n) = 0
[PROOF STEP]
by (cases n)
       (simp_all del: funpow.simps add: funpow_Suc_right pderiv_monom pochhammer_rec' Suc.IH)
[PROOF STATE]
proof (state)
this:
(pderiv ^^ Suc m) (Polynomial.monom c n) = 0

goal (1 subgoal):
 1. \<And>c n. n + 1 < 0 \<Longrightarrow> (pderiv ^^ 0) (Polynomial.monom c n) = 0
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma higher_pderiv_sum: "(pderiv ^^ n) (sum f A) = (\<Sum>x\<in>A. (pderiv ^^ n) (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pderiv ^^ n) (sum f A) = (\<Sum>x\<in>A. (pderiv ^^ n) (f x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) (simp_all add: higher_pderiv_add)


[STATEMENT]
lemma fact_dvd_higher_pderiv:
  "[:fact n :: int:] dvd (pderiv ^^ n) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:fact n:] dvd (pderiv ^^ n) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [:fact n:] dvd (pderiv ^^ n) p
[PROOF STEP]
have "[:fact n:] dvd (pderiv ^^ n) (monom c k)" for c :: int and k :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:fact n:] dvd (pderiv ^^ n) (Polynomial.monom c k)
[PROOF STEP]
by (cases "n \<le> k + 1")
       (simp_all add: higher_pderiv_monom higher_pderiv_monom_eq_zero
          fact_dvd_pochhammer const_poly_dvd_iff)
[PROOF STATE]
proof (state)
this:
[:fact n:] dvd (pderiv ^^ n) (Polynomial.monom ?c ?k)

goal (1 subgoal):
 1. [:fact n:] dvd (pderiv ^^ n) p
[PROOF STEP]
hence "[:fact n:] dvd (pderiv ^^ n) (\<Sum>k\<le>degree p. monom (coeff p k) k)"
[PROOF STATE]
proof (prove)
using this:
[:fact n:] dvd (pderiv ^^ n) (Polynomial.monom ?c ?k)

goal (1 subgoal):
 1. [:fact n:] dvd (pderiv ^^ n) (\<Sum>k\<le>degree p. Polynomial.monom (poly.coeff p k) k)
[PROOF STEP]
by (simp_all add: higher_pderiv_sum dvd_sum)
[PROOF STATE]
proof (state)
this:
[:fact n:] dvd (pderiv ^^ n) (\<Sum>k\<le>degree p. Polynomial.monom (poly.coeff p k) k)

goal (1 subgoal):
 1. [:fact n:] dvd (pderiv ^^ n) p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[:fact n:] dvd (pderiv ^^ n) (\<Sum>k\<le>degree p. Polynomial.monom (poly.coeff p k) k)

goal (1 subgoal):
 1. [:fact n:] dvd (pderiv ^^ n) p
[PROOF STEP]
by (simp add: poly_as_sum_of_monoms)
[PROOF STATE]
proof (state)
this:
[:fact n:] dvd (pderiv ^^ n) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fact_dvd_poly_higher_pderiv_aux:
  "(fact n :: int) dvd poly ((pderiv ^^ n) p) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ n) p) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ n) p) x
[PROOF STEP]
have "[:fact n:] dvd (pderiv ^^ n) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:fact n:] dvd (pderiv ^^ n) p
[PROOF STEP]
by (rule fact_dvd_higher_pderiv)
[PROOF STATE]
proof (state)
this:
[:fact n:] dvd (pderiv ^^ n) p

goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ n) p) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[:fact n:] dvd (pderiv ^^ n) p
[PROOF STEP]
obtain q where "(pderiv ^^ n) p = [:fact n:] * q"
[PROOF STATE]
proof (prove)
using this:
[:fact n:] dvd (pderiv ^^ n) p

goal (1 subgoal):
 1. (\<And>q. (pderiv ^^ n) p = [:fact n:] * q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule dvdE)
[PROOF STATE]
proof (state)
this:
(pderiv ^^ n) p = [:fact n:] * q

goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ n) p) x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(pderiv ^^ n) p = [:fact n:] * q

goal (1 subgoal):
 1. fact n dvd poly ((pderiv ^^ n) p) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fact n dvd poly ((pderiv ^^ n) p) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fact_dvd_poly_higher_pderiv_aux':
  "m \<le> n \<Longrightarrow> (fact m :: int) dvd poly ((pderiv ^^ n) p) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> fact m dvd poly ((pderiv ^^ n) p) x
[PROOF STEP]
by (rule dvd_trans[OF fact_dvd fact_dvd_poly_higher_pderiv_aux]) simp_all


[STATEMENT]
lemma algebraicE':
  assumes "algebraic (x :: 'a :: field_char_0)"
  obtains p where "p \<noteq> 0" "poly (of_int_poly p) x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
algebraic x
[PROOF STEP]
obtain q where "\<And>i. coeff q i \<in> \<int>" "q \<noteq> 0" "poly q x = 0"
[PROOF STATE]
proof (prove)
using this:
algebraic x

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>\<And>i. poly.coeff q i \<in> \<int>; q \<noteq> 0; poly q x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule algebraicE)
[PROOF STATE]
proof (state)
this:
poly.coeff q ?i \<in> \<int>
q \<noteq> 0
poly q x = (0::'a)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poly.coeff q ?i \<in> \<int>
q \<noteq> 0
poly q x = (0::'a)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
poly.coeff q ?i \<in> \<int>
[PROOF STEP]
obtain q' where "q = of_int_poly q'"
[PROOF STATE]
proof (prove)
using this:
poly.coeff q ?i \<in> \<int>

goal (1 subgoal):
 1. (\<And>q'. q = of_int_poly q' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule int_polyE)
[PROOF STATE]
proof (state)
this:
q = of_int_poly q'

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
poly.coeff q ?i \<in> \<int>
q \<noteq> 0
poly q x = (0::'a)
q = of_int_poly q'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly.coeff q ?i \<in> \<int>
q \<noteq> 0
poly q x = (0::'a)
q = of_int_poly q'

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (intro that[of q']) simp_all
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma algebraicE'_nonzero:
  assumes "algebraic (x :: 'a :: field_char_0)" "x \<noteq> 0"
  obtains p where "p \<noteq> 0" "coeff p 0 \<noteq> 0" "poly (of_int_poly p) x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
algebraic x
[PROOF STEP]
obtain p where p: "p \<noteq> 0" "poly (of_int_poly p) x = 0"
[PROOF STATE]
proof (prove)
using this:
algebraic x

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule algebraicE')
[PROOF STATE]
proof (state)
this:
p \<noteq> 0
poly (of_int_poly p) x = (0::'a)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define n :: nat where "n = order 0 p"
[PROOF STATE]
proof (state)
this:
n = Polynomial.order 0 p

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "monom 1 n dvd p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.monom 1 n dvd p
[PROOF STEP]
by (simp add: monom_1_dvd_iff p n_def)
[PROOF STATE]
proof (state)
this:
Polynomial.monom 1 n dvd p

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Polynomial.monom 1 n dvd p
[PROOF STEP]
obtain q where q: "p = monom 1 n * q"
[PROOF STATE]
proof (prove)
using this:
Polynomial.monom 1 n dvd p

goal (1 subgoal):
 1. (\<And>q. p = Polynomial.monom 1 n * q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule dvdE)
[PROOF STATE]
proof (state)
this:
p = Polynomial.monom 1 n * q

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 0
poly (of_int_poly p) x = (0::'a)
[PROOF STEP]
have "q \<noteq> 0" "poly (of_int_poly q) x = 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
poly (of_int_poly p) x = (0::'a)

goal (1 subgoal):
 1. q \<noteq> 0 &&& poly (of_int_poly q) x = (0::'a)
[PROOF STEP]
by (auto simp: q poly_monom assms(2))
[PROOF STATE]
proof (state)
this:
q \<noteq> 0
poly (of_int_poly q) x = (0::'a)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
q \<noteq> 0
poly (of_int_poly q) x = (0::'a)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> 0
poly (of_int_poly q) x = (0::'a)
[PROOF STEP]
have "order 0 p = n + order 0 q"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0
poly (of_int_poly q) x = (0::'a)

goal (1 subgoal):
 1. Polynomial.order 0 p = n + Polynomial.order 0 q
[PROOF STEP]
by (simp add: q order_mult)
[PROOF STATE]
proof (state)
this:
Polynomial.order 0 p = n + Polynomial.order 0 q

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "order 0 q = 0"
[PROOF STATE]
proof (prove)
using this:
Polynomial.order 0 p = n + Polynomial.order 0 q

goal (1 subgoal):
 1. Polynomial.order 0 q = 0
[PROOF STEP]
by (simp add: n_def)
[PROOF STATE]
proof (state)
this:
Polynomial.order 0 q = 0

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>q \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> 0
Polynomial.order 0 q = 0
[PROOF STEP]
have "poly q 0 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0
Polynomial.order 0 q = 0

goal (1 subgoal):
 1. poly q 0 \<noteq> 0
[PROOF STEP]
by (simp add: order_root)
[PROOF STATE]
proof (state)
this:
poly q 0 \<noteq> 0

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly.coeff p 0 \<noteq> 0; poly (of_int_poly p) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> 0
poly (of_int_poly q) x = (0::'a)
poly q 0 \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0
poly (of_int_poly q) x = (0::'a)
poly q 0 \<noteq> 0

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of q]
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0
poly (of_int_poly q) x = (0::'a)
poly q 0 \<noteq> 0
\<lbrakk>q \<noteq> 0; poly.coeff q 0 \<noteq> 0; poly (of_int_poly q) x = (0::'a)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto simp: poly_0_coeff_0)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma algebraic_of_real_iff [simp]:
   "algebraic (of_real x :: 'a :: {real_algebra_1,field_char_0}) \<longleftrightarrow> algebraic x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. algebraic (of_real x) = algebraic x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. algebraic (of_real x) \<Longrightarrow> algebraic x
 2. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
assume "algebraic (of_real x :: 'a)"
[PROOF STATE]
proof (state)
this:
algebraic (of_real x)

goal (2 subgoals):
 1. algebraic (of_real x) \<Longrightarrow> algebraic x
 2. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
algebraic (of_real x)
[PROOF STEP]
obtain p where "p \<noteq> 0" "poly (of_int_poly p) (of_real x :: 'a) = 0"
[PROOF STATE]
proof (prove)
using this:
algebraic (of_real x)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly (of_int_poly p) (of_real x) = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule algebraicE')
[PROOF STATE]
proof (state)
this:
p \<noteq> 0
poly (of_int_poly p) (of_real x) = (0::'a)

goal (2 subgoals):
 1. algebraic (of_real x) \<Longrightarrow> algebraic x
 2. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
hence "(of_int_poly p :: real poly) \<noteq> 0"
        "poly (of_int_poly p :: real poly) x = 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
poly (of_int_poly p) (of_real x) = (0::'a)

goal (1 subgoal):
 1. of_int_poly p \<noteq> 0 &&& poly (of_int_poly p) x = 0
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
of_int_poly p \<noteq> 0
poly (of_int_poly p) x = 0

goal (2 subgoals):
 1. algebraic (of_real x) \<Longrightarrow> algebraic x
 2. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
thus "algebraic x"
[PROOF STATE]
proof (prove)
using this:
of_int_poly p \<noteq> 0
poly (of_int_poly p) x = 0

goal (1 subgoal):
 1. algebraic x
[PROOF STEP]
by (intro algebraicI[of "of_int_poly p"]) simp_all
[PROOF STATE]
proof (state)
this:
algebraic x

goal (1 subgoal):
 1. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
assume "algebraic x"
[PROOF STATE]
proof (state)
this:
algebraic x

goal (1 subgoal):
 1. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
algebraic x
[PROOF STEP]
obtain p where "p \<noteq> 0" "poly (of_int_poly p) x = 0"
[PROOF STATE]
proof (prove)
using this:
algebraic x

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<noteq> 0; poly (of_int_poly p) x = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule algebraicE')
[PROOF STATE]
proof (state)
this:
p \<noteq> 0
poly (of_int_poly p) x = 0

goal (1 subgoal):
 1. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
hence "of_int_poly p \<noteq> (0 :: 'a poly)" "poly (of_int_poly p) (of_real x :: 'a) = 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
poly (of_int_poly p) x = 0

goal (1 subgoal):
 1. of_int_poly p \<noteq> 0 &&& poly (of_int_poly p) (of_real x) = (0::'a)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
of_int_poly p \<noteq> 0
poly (of_int_poly p) (of_real x) = (0::'a)

goal (1 subgoal):
 1. algebraic x \<Longrightarrow> algebraic (of_real x)
[PROOF STEP]
thus "algebraic (of_real x)"
[PROOF STATE]
proof (prove)
using this:
of_int_poly p \<noteq> 0
poly (of_int_poly p) (of_real x) = (0::'a)

goal (1 subgoal):
 1. algebraic (of_real x)
[PROOF STEP]
by (intro algebraicI[of "of_int_poly p"]) simp_all
[PROOF STATE]
proof (state)
this:
algebraic (of_real x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lindemann_weierstrass_integral:
  fixes u :: complex and f :: "complex poly"
  defines "df \<equiv> \<lambda>n. (pderiv ^^ n) f"
  defines "m \<equiv> degree f"
  defines "I \<equiv> \<lambda>f u. exp u * (\<Sum>j\<le>degree f. poly ((pderiv ^^ j) f) 0) -
                       (\<Sum>j\<le>degree f. poly ((pderiv ^^ j) f) u)"
  shows "((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)
[PROOF STEP]
note [derivative_intros] =
    exp_scaleR_has_vector_derivative_right vector_diff_chain_within
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (t *\<^sub>R ?A)) has_vector_derivative exp (?t *\<^sub>R ?A) * ?A) (at ?t within ?T)
\<lbrakk>(?f has_vector_derivative ?f') (at ?x within ?s); (?g has_vector_derivative ?g') (at (?f ?x) within ?f ` ?s)\<rbrakk> \<Longrightarrow> (?g \<circ> ?f has_vector_derivative ?f' *\<^sub>R ?g') (at ?x within ?s)

goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)
[PROOF STEP]
let ?g = "\<lambda>t. 1 - t" and ?f = "\<lambda>t. -exp (t *\<^sub>R u)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)
[PROOF STEP]
have "((\<lambda>t. exp ((1 - t) *\<^sub>R u) * u) has_integral
          (?f \<circ> ?g) 1 - (?f \<circ> ?g) 0) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. exp ((1 - t) *\<^sub>R u) * u) has_integral ((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1) 1 - ((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1) 0) {0..1}
[PROOF STEP]
by (rule fundamental_theorem_of_calculus)
       (auto intro!: derivative_eq_intros simp del: o_apply)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp ((1 - t) *\<^sub>R u) * u) has_integral ((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1) 1 - ((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1) 0) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)
[PROOF STEP]
hence aux_integral: "((\<lambda>t. exp (u - t *\<^sub>R u) * u) has_integral exp u - 1) {0..1}"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. exp ((1 - t) *\<^sub>R u) * u) has_integral ((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1) 1 - ((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1) 0) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t *\<^sub>R u) * u) has_integral exp u - 1) {0..1}
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u) has_integral exp u - 1) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)
[PROOF STEP]
have "((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
unfolding df_def m_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
proof (induction "degree f" arbitrary: f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f. 0 = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
 2. \<And>x f. \<lbrakk>\<And>f. x = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}; Suc x = degree f\<rbrakk> \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = degree f

goal (2 subgoals):
 1. \<And>f. 0 = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
 2. \<And>x f. \<lbrakk>\<And>f. x = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}; Suc x = degree f\<rbrakk> \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = degree f
[PROOF STEP]
obtain c where c: "f = [:c:]"
[PROOF STATE]
proof (prove)
using this:
0 = degree f

goal (1 subgoal):
 1. (\<And>c. f = [:c:] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: degree_eq_zeroE)
[PROOF STATE]
proof (state)
this:
f = [:c:]

goal (2 subgoals):
 1. \<And>f. 0 = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
 2. \<And>x f. \<lbrakk>\<And>f. x = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}; Suc x = degree f\<rbrakk> \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
have "((\<lambda>t. c * (exp (u - t *\<^sub>R u) * u)) has_integral c * (exp u - 1)) {0..1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. c * (exp (u - t *\<^sub>R u) * u)) has_integral c * (exp u - 1)) {0..1}
[PROOF STEP]
using aux_integral
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u) has_integral exp u - 1) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. c * (exp (u - t *\<^sub>R u) * u)) has_integral c * (exp u - 1)) {0..1}
[PROOF STEP]
by (rule has_integral_mult_right)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. c * (exp (u - t *\<^sub>R u) * u)) has_integral c * (exp u - 1)) {0..1}

goal (2 subgoals):
 1. \<And>f. 0 = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
 2. \<And>x f. \<lbrakk>\<And>f. x = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}; Suc x = degree f\<rbrakk> \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
with c
[PROOF STATE]
proof (chain)
picking this:
f = [:c:]
((\<lambda>t. c * (exp (u - t *\<^sub>R u) * u)) has_integral c * (exp u - 1)) {0..1}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f = [:c:]
((\<lambda>t. c * (exp (u - t *\<^sub>R u) * u)) has_integral c * (exp u - 1)) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
by (simp add: algebra_simps I_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}

goal (1 subgoal):
 1. \<And>x f. \<lbrakk>\<And>f. x = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}; Suc x = degree f\<rbrakk> \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x f. \<lbrakk>\<And>f. x = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}; Suc x = degree f\<rbrakk> \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
m = degree ?f1 \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly ?f1 (t *\<^sub>R u)) has_integral I ?f1 u) {0..1}
Suc m = degree f

goal (1 subgoal):
 1. \<And>x f. \<lbrakk>\<And>f. x = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}; Suc x = degree f\<rbrakk> \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
define df where "df = (\<lambda>j. (pderiv ^^ j) f)"
[PROOF STATE]
proof (state)
this:
df = (\<lambda>j. (pderiv ^^ j) f)

goal (1 subgoal):
 1. \<And>x f. \<lbrakk>\<And>f. x = degree f \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}; Suc x = degree f\<rbrakk> \<Longrightarrow> ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}
[PROOF STEP]
proof (rule integration_by_parts[OF bounded_bilinear_mult])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} ?f
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> (?f has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)
 5. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 6. ((\<lambda>t. ?f t * ?g' t) has_integral ?f 1 * poly f (1 *\<^sub>R u) - ?f 0 * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
fix t :: real
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} ?f
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> (?f has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)
 5. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 6. ((\<lambda>t. ?f t * ?g' t) has_integral ?f 1 * poly f (1 *\<^sub>R u) - ?f 0 * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
assume "t \<in> {0..1}"
[PROOF STATE]
proof (state)
this:
t \<in> {0..1}

goal (6 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} ?f
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> (?f has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)
 5. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 6. ((\<lambda>t. ?f t * ?g' t) has_integral ?f 1 * poly f (1 *\<^sub>R u) - ?f 0 * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
have "((?f \<circ> ?g) has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1 has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)
[PROOF STEP]
by (auto intro!: derivative_eq_intros simp: algebra_simps simp del: o_apply)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1 has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)

goal (6 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} ?f
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> (?f has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)
 5. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 6. ((\<lambda>t. ?f t * ?g' t) has_integral ?f 1 * poly f (1 *\<^sub>R u) - ?f 0 * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
thus "((\<lambda>t. -exp (u - t *\<^sub>R u)) has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. - exp (t *\<^sub>R u)) \<circ> (-) 1 has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)

goal (1 subgoal):
 1. ((\<lambda>t. - exp (u - t *\<^sub>R u)) has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)
[PROOF STEP]
by (simp add: algebra_simps o_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. - exp (u - t *\<^sub>R u)) has_vector_derivative exp (u - t *\<^sub>R u) * u) (at t)

goal (5 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 5. ((\<lambda>t. - exp (u - t *\<^sub>R u) * ?g' t) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 5. ((\<lambda>t. - exp (u - t *\<^sub>R u) * ?g' t) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
fix t :: real
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 5. ((\<lambda>t. - exp (u - t *\<^sub>R u) * ?g' t) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
assume "t \<in> {0..1}"
[PROOF STATE]
proof (state)
this:
t \<in> {0..1}

goal (5 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 5. ((\<lambda>t. - exp (u - t *\<^sub>R u) * ?g' t) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
have "(poly f \<circ> (\<lambda>t. t *\<^sub>R u) has_vector_derivative u * poly (pderiv f) (t *\<^sub>R u)) (at t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly f \<circ> (\<lambda>t. t *\<^sub>R u) has_vector_derivative u * poly (pderiv f) (t *\<^sub>R u)) (at t)
[PROOF STEP]
by (rule field_vector_diff_chain_at) (auto intro!: derivative_eq_intros)
[PROOF STATE]
proof (state)
this:
(poly f \<circ> (\<lambda>t. t *\<^sub>R u) has_vector_derivative u * poly (pderiv f) (t *\<^sub>R u)) (at t)

goal (5 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. \<And>t. t \<in> {0..1} \<Longrightarrow> ((\<lambda>x. poly f (x *\<^sub>R u)) has_vector_derivative ?g' t) (at t)
 5. ((\<lambda>t. - exp (u - t *\<^sub>R u) * ?g' t) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
thus "((\<lambda>t. poly f (t *\<^sub>R u)) has_vector_derivative u * poly (pderiv f) (t *\<^sub>R u)) (at t)"
[PROOF STATE]
proof (prove)
using this:
(poly f \<circ> (\<lambda>t. t *\<^sub>R u) has_vector_derivative u * poly (pderiv f) (t *\<^sub>R u)) (at t)

goal (1 subgoal):
 1. ((\<lambda>t. poly f (t *\<^sub>R u)) has_vector_derivative u * poly (pderiv f) (t *\<^sub>R u)) (at t)
[PROOF STEP]
by (simp add: o_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. poly f (t *\<^sub>R u)) has_vector_derivative u * poly (pderiv f) (t *\<^sub>R u)) (at t)

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
from Suc(2)
[PROOF STATE]
proof (chain)
picking this:
Suc m = degree f
[PROOF STEP]
have m: "m = degree (pderiv f)"
[PROOF STATE]
proof (prove)
using this:
Suc m = degree f

goal (1 subgoal):
 1. m = degree (pderiv f)
[PROOF STEP]
by (simp add: degree_pderiv)
[PROOF STATE]
proof (state)
this:
m = degree (pderiv f)

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
from Suc(1)[OF this] this
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u)) has_integral I (pderiv f) u) {0..1}
m = degree (pderiv f)
[PROOF STEP]
have "((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u)) has_integral
                exp u * (\<Sum>j=0..m. poly (df (Suc j)) 0) - (\<Sum>j=0..m. poly (df (Suc j)) u)) {0..1}"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u)) has_integral I (pderiv f) u) {0..1}
m = degree (pderiv f)

goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u)) has_integral exp u * (\<Sum>j = 0..m. poly (df (Suc j)) 0) - (\<Sum>j = 0..m. poly (df (Suc j)) u)) {0..1}
[PROOF STEP]
by (simp add: df_def funpow_swap1 atMost_atLeast0 I_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u)) has_integral exp u * (\<Sum>j = 0..m. poly (df (Suc j)) 0) - (\<Sum>j = 0..m. poly (df (Suc j)) u)) {0..1}

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u)) has_integral exp u * (\<Sum>j = 0..m. poly (df (Suc j)) 0) - (\<Sum>j = 0..m. poly (df (Suc j)) u)) {0..1}

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
have "(\<Sum>j=0..m. poly (df (Suc j)) 0) = (\<Sum>j=Suc 0..Suc m. poly (df j) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..m. poly (df (Suc j)) 0) = (\<Sum>j = Suc 0..Suc m. poly (df j) 0)
[PROOF STEP]
by (rule sum.shift_bounds_cl_Suc_ivl [symmetric])
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..m. poly (df (Suc j)) 0) = (\<Sum>j = Suc 0..Suc m. poly (df j) 0)

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..m. poly (df (Suc j)) 0) = (\<Sum>j = Suc 0..Suc m. poly (df j) 0)

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
have "\<dots> = (\<Sum>j=0..Suc m. poly (df j) 0) - poly f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = Suc 0..Suc m. poly (df j) 0) = (\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0
[PROOF STEP]
by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: df_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = Suc 0..Suc m. poly (df j) 0) = (\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = Suc 0..Suc m. poly (df j) 0) = (\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
have "(\<Sum>j=0..m. poly (df (Suc j)) u) = (\<Sum>j=Suc 0..Suc m. poly (df j) u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..m. poly (df (Suc j)) u) = (\<Sum>j = Suc 0..Suc m. poly (df j) u)
[PROOF STEP]
by (rule sum.shift_bounds_cl_Suc_ivl [symmetric])
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..m. poly (df (Suc j)) u) = (\<Sum>j = Suc 0..Suc m. poly (df j) u)

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..m. poly (df (Suc j)) u) = (\<Sum>j = Suc 0..Suc m. poly (df j) u)

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
have "\<dots> = (\<Sum>j=0..Suc m. poly (df j) u) - poly f u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = Suc 0..Suc m. poly (df j) u) = (\<Sum>j = 0..Suc m. poly (df j) u) - poly f u
[PROOF STEP]
by (subst (2) sum.atLeast_Suc_atMost) (simp_all add: df_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = Suc 0..Suc m. poly (df j) u) = (\<Sum>j = 0..Suc m. poly (df j) u) - poly f u

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u)) has_integral exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) - ((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u)) {0..1}
[PROOF STEP]
have "((\<lambda>t. - (exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u))) has_integral
                        -(exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) -
                                  ((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u))) {0..1}"
          (is "(_ has_integral ?I) _")
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u)) has_integral exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) - ((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u)) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. - (exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u))) has_integral - (exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) - ((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u))) {0..1}
[PROOF STEP]
by (rule has_integral_neg)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. - (exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u))) has_integral - (exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) - ((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u))) {0..1}

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>t. - (exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u))) has_integral - (exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) - ((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u))) {0..1}

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
have "?I = - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) -
                       - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) - ((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u)) = - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u
[PROOF STEP]
by (simp add: df_def algebra_simps Suc(2) atMost_atLeast0 I_def)
[PROOF STATE]
proof (state)
this:
- (exp u * ((\<Sum>j = 0..Suc m. poly (df j) 0) - poly f 0) - ((\<Sum>j = 0..Suc m. poly (df j) u) - poly f u)) = - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u

goal (4 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
 4. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>t. - (exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
show "((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u)))
                        has_integral \<dots>) {0..1}"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. - (exp (u - t *\<^sub>R u) * u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. - exp (u - t *\<^sub>R u) * (u * poly (pderiv f) (t *\<^sub>R u))) has_integral - exp (u - 1 *\<^sub>R u) * poly f (1 *\<^sub>R u) - - exp (u - 0 *\<^sub>R u) * poly f (0 *\<^sub>R u) - I f u) {0..1}

goal (3 subgoals):
 1. 0 \<le> 1
 2. continuous_on {0..1} (\<lambda>t. - exp (u - t *\<^sub>R u))
 3. continuous_on {0..1} (\<lambda>x. poly f (x *\<^sub>R u))
[PROOF STEP]
qed (auto intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>t. exp (u - t *\<^sub>R u) * u * poly f (t *\<^sub>R u)) has_integral I f u) {0..1}

goal (1 subgoal):
 1. ((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)
[PROOF STEP]
by (simp add: has_contour_integral_linepath algebra_simps)
[PROOF STATE]
proof (state)
this:
((\<lambda>t. exp (u - t) * poly f t) has_contour_integral I f u) (linepath 0 u)

goal:
No subgoals!
[PROOF STEP]
qed