[STATEMENT]
lemma hensel_1:
  fixes u :: "'pq :: nontriv mod_ring poly"
    and v w :: "'q :: nontriv mod_ring poly"
  assumes "CARD('pq) = CARD('p :: prime_card) * CARD('q)"
      and "CARD('p) dvd CARD('q)"
      and uvw: "#u = v * w"
      and degu: "degree u = degree v + degree w"
      and monic: "monic v"
      and coprime: "coprime (#v :: 'p mod_ring poly) (#w)"
      and out: "hensel_1 TYPE('p) u v w = (V',W')"
  shows "u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and>
         monic V' \<and> coprime (#V' :: 'p mod_ring poly) (#W')" (is ?main)
    and "(\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow>
          degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow>
          V'' = V' \<and> W'' = W')" (is "?unique")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W') &&& \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from monic
[PROOF STATE]
proof (chain)
picking this:
monic v
[PROOF STEP]
have degv: "degree (#v :: 'p mod_ring poly) = degree v"
[PROOF STATE]
proof (prove)
using this:
monic v

goal (1 subgoal):
 1. degree (#v) = degree v
[PROOF STEP]
by (simp add: of_int_hom.monic_degree_map_poly_hom)
[PROOF STATE]
proof (state)
this:
degree (#v) = degree v

goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from monic
[PROOF STATE]
proof (chain)
picking this:
monic v
[PROOF STEP]
have monic2: "monic (#v :: 'p mod_ring poly)"
[PROOF STATE]
proof (prove)
using this:
monic v

goal (1 subgoal):
 1. monic (#v)
[PROOF STEP]
by (auto simp: degv)
[PROOF STATE]
proof (state)
this:
monic (#v)

goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
obtain s t where bezout: "bezout_coefficients (#v :: 'p mod_ring poly) (#w) = (s, t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s t. bezout_coefficients (#v) (#w) = (s, t) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: prod_eq_iff)
[PROOF STATE]
proof (state)
this:
bezout_coefficients (#v) (#w) = (s, t)

goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bezout_coefficients (#v) (#w) = (s, t)
[PROOF STEP]
have "s * #v + t * #w = gcd (#v :: 'p mod_ring poly) (#w)"
[PROOF STATE]
proof (prove)
using this:
bezout_coefficients (#v) (#w) = (s, t)

goal (1 subgoal):
 1. s * #v + t * #w = gcd (#v) (#w)
[PROOF STEP]
by (rule bezout_coefficients)
[PROOF STATE]
proof (state)
this:
s * #v + t * #w = gcd (#v) (#w)

goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
with coprime
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime (#v) (#w)
s * #v + t * #w = gcd (#v) (#w)
[PROOF STEP]
have vswt: "#v * s + #w * t = 1"
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime (#v) (#w)
s * #v + t * #w = gcd (#v) (#w)

goal (1 subgoal):
 1. #v * s + #w * t = 1
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
#v * s + #w * t = 1

goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
obtain a b where dupe: "dupe_monic (#v) (#w) s t 1 = (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. Hensel_Lifting_Type_Based.dupe_monic (#v) (#w) s t 1 = (a, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Hensel_Lifting_Type_Based.dupe_monic (#v) (#w) s t 1 = (a, b)

goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from dupe_monic(1,2)[OF vswt monic2, where U=1, unfolded this]
[PROOF STATE]
proof (chain)
picking this:
(a, b) = (?A, ?B) \<Longrightarrow> ?A * #v + ?B * #w = 1
(a, b) = (?A, ?B) \<Longrightarrow> ?B = 0 \<or> degree ?B < degree (#v)
[PROOF STEP]
have avbw: "a * #v + b * #w = 1" and degb: "b = 0 \<or> degree b < degree (#v::'p mod_ring poly)"
[PROOF STATE]
proof (prove)
using this:
(a, b) = (?A, ?B) \<Longrightarrow> ?A * #v + ?B * #w = 1
(a, b) = (?A, ?B) \<Longrightarrow> ?B = 0 \<or> degree ?B < degree (#v)

goal (1 subgoal):
 1. a * #v + b * #w = 1 &&& b = 0 \<or> degree b < degree (#v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a * #v + b * #w = 1
b = 0 \<or> degree b < degree (#v)

goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
have "?main \<and> ?unique"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
proof (cases "b = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
 2. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
case b0: True
[PROOF STATE]
proof (state)
this:
b = 0

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
 2. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
with avbw
[PROOF STATE]
proof (chain)
picking this:
a * #v + b * #w = 1
b = 0
[PROOF STEP]
have "a * #v = 1"
[PROOF STATE]
proof (prove)
using this:
a * #v + b * #w = 1
b = 0

goal (1 subgoal):
 1. a * #v = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a * #v = 1

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
 2. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a * #v = 1
[PROOF STEP]
have "degree (#v :: 'p mod_ring poly) = 0"
[PROOF STATE]
proof (prove)
using this:
a * #v = 1

goal (1 subgoal):
 1. degree (#v) = 0
[PROOF STEP]
by (metis degree_1 degree_mult_eq_0 mult_zero_left one_neq_zero)
[PROOF STATE]
proof (state)
this:
degree (#v) = 0

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
 2. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
from this[unfolded degv] monic_degree_0[OF monic[unfolded]]
[PROOF STATE]
proof (chain)
picking this:
degree v = 0
(degree v = 0) = (v = 1)
[PROOF STEP]
have 1: "v = 1"
[PROOF STATE]
proof (prove)
using this:
degree v = 0
(degree v = 0) = (v = 1)

goal (1 subgoal):
 1. v = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = 1

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
 2. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
with b0 out uvw
[PROOF STATE]
proof (chain)
picking this:
b = 0
hensel_1 TYPE('p) u v w = (V', W')
#u = v * w
v = 1
[PROOF STEP]
have 2: "V' = 1" "W' = u"
[PROOF STATE]
proof (prove)
using this:
b = 0
hensel_1 TYPE('p) u v w = (V', W')
#u = v * w
v = 1

goal (1 subgoal):
 1. V' = 1 &&& W' = u
[PROOF STEP]
by (unfold split hensel_1_def Let_def dupe) auto
[PROOF STATE]
proof (state)
this:
V' = 1
W' = u

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
 2. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
have 3: ?unique
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
apply (simp add: 1 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> #V'' = 1 \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = 0 \<longrightarrow> degree W'' = degree (#W'') \<longrightarrow> poly.coeff V'' 0 = 1 \<longrightarrow> V'' = 1 \<and> W'' = V'' * W''
[PROOF STEP]
by (metis monic_degree_0 mult.left_neutral)
[PROOF STATE]
proof (state)
this:
\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
 2. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
with uvw degu
[PROOF STATE]
proof (chain)
picking this:
#u = v * w
degree u = degree v + degree w
\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
#u = v * w
degree u = degree v + degree w
\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'

goal (1 subgoal):
 1. (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
unfolding 1 2
[PROOF STATE]
proof (prove)
using this:
#u = 1 * w
degree u = degree 1 + degree w
\<forall>V'' W''. u = V'' * W'' \<longrightarrow> 1 = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree 1 \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff 1 \<longrightarrow> V'' = 1 \<and> W'' = u

goal (1 subgoal):
 1. (u = 1 * u \<and> 1 = #1 \<and> w = #u \<and> degree 1 = degree 1 \<and> degree u = degree w \<and> monic 1 \<and> comm_monoid_mult_class.coprime (#1) (#u)) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> 1 = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree 1 \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff 1 \<longrightarrow> V'' = 1 \<and> W'' = u)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
case b0: False
[PROOF STATE]
proof (state)
this:
b \<noteq> 0

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
with degb degv
[PROOF STATE]
proof (chain)
picking this:
b = 0 \<or> degree b < degree (#v)
degree (#v) = degree v
b \<noteq> 0
[PROOF STEP]
have degb: "degree b < degree v"
[PROOF STATE]
proof (prove)
using this:
b = 0 \<or> degree b < degree (#v)
degree (#v) = degree v
b \<noteq> 0

goal (1 subgoal):
 1. degree b < degree v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree b < degree v

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree b < degree v
[PROOF STEP]
have v1: "v \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
degree b < degree v

goal (1 subgoal):
 1. v \<noteq> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<noteq> 1

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
interpret Knuth_ex_4_6_2_22_prime "TYPE('p)" "TYPE('q)" "TYPE('pq)" a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Knuth_ex_4_6_2_22_prime a b u v w
[PROOF STEP]
by (unfold_locales; fact assms degb avbw)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
proof (intro conjI)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. u = V' * W'
 2. v = #V'
 3. w = #W'
 4. degree V' = degree v
 5. degree W' = degree w
 6. monic V'
 7. comm_monoid_mult_class.coprime (#V') (#W')
 8. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from out [unfolded hensel_1_def] v1
[PROOF STATE]
proof (chain)
picking this:
(if v = 1 then (1, u) else let (s, t) = bezout_coefficients (#v) (#w); (a, b) = Hensel_Lifting_Type_Based.dupe_monic (#v) (#w) s t 1 in (#v + Polynomial.smult (of_nat q) (#Knuth_ex_4_6_2_22_main.v' TYPE('q) b u v w), #w + Polynomial.smult (of_nat q) (#Knuth_ex_4_6_2_22_main.w' TYPE('q) a b u v w))) = (V', W')
v \<noteq> 1
[PROOF STEP]
have 1 [simp]: "V' = V" "W' = W"
[PROOF STATE]
proof (prove)
using this:
(if v = 1 then (1, u) else let (s, t) = bezout_coefficients (#v) (#w); (a, b) = Hensel_Lifting_Type_Based.dupe_monic (#v) (#w) s t 1 in (#v + Polynomial.smult (of_nat q) (#Knuth_ex_4_6_2_22_main.v' TYPE('q) b u v w), #w + Polynomial.smult (of_nat q) (#Knuth_ex_4_6_2_22_main.w' TYPE('q) a b u v w))) = (V', W')
v \<noteq> 1

goal (1 subgoal):
 1. V' = #v + Polynomial.smult (of_nat q) (#v') &&& W' = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
by (auto simp: bezout dupe)
[PROOF STATE]
proof (state)
this:
V' = #v + Polynomial.smult (of_nat q) (#v')
W' = #w + Polynomial.smult (of_nat q) (#w')

goal (8 subgoals):
 1. u = V' * W'
 2. v = #V'
 3. w = #W'
 4. degree V' = degree v
 5. degree W' = degree w
 6. monic V'
 7. comm_monoid_mult_class.coprime (#V') (#W')
 8. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from uVW
[PROOF STATE]
proof (chain)
picking this:
u = (#v + Polynomial.smult (of_nat q) (#v')) * (#w + Polynomial.smult (of_nat q) (#w'))
[PROOF STEP]
show "u = V' * W'"
[PROOF STATE]
proof (prove)
using this:
u = (#v + Polynomial.smult (of_nat q) (#v')) * (#w + Polynomial.smult (of_nat q) (#w'))

goal (1 subgoal):
 1. u = V' * W'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u = V' * W'

goal (7 subgoals):
 1. v = #V'
 2. w = #W'
 3. degree V' = degree v
 4. degree W' = degree w
 5. monic V'
 6. comm_monoid_mult_class.coprime (#V') (#W')
 7. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from degV
[PROOF STATE]
proof (chain)
picking this:
degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
[PROOF STEP]
show [simp]: "degree V' = degree v"
[PROOF STATE]
proof (prove)
using this:
degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v

goal (1 subgoal):
 1. degree V' = degree v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree V' = degree v

goal (6 subgoals):
 1. v = #V'
 2. w = #W'
 3. degree W' = degree w
 4. monic V'
 5. comm_monoid_mult_class.coprime (#V') (#W')
 6. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from degW
[PROOF STATE]
proof (chain)
picking this:
degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
show [simp]: "degree W' = degree w"
[PROOF STATE]
proof (prove)
using this:
degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w

goal (1 subgoal):
 1. degree W' = degree w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree W' = degree w

goal (5 subgoals):
 1. v = #V'
 2. w = #W'
 3. monic V'
 4. comm_monoid_mult_class.coprime (#V') (#W')
 5. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from lcV
[PROOF STATE]
proof (chain)
picking this:
lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
[PROOF STEP]
have "lead_coeff V' = @lead_coeff v"
[PROOF STATE]
proof (prove)
using this:
lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v

goal (1 subgoal):
 1. lead_coeff V' = @lead_coeff v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lead_coeff V' = @lead_coeff v

goal (5 subgoals):
 1. v = #V'
 2. w = #W'
 3. monic V'
 4. comm_monoid_mult_class.coprime (#V') (#W')
 5. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
with monic_v
[PROOF STATE]
proof (chain)
picking this:
monic v
lead_coeff V' = @lead_coeff v
[PROOF STEP]
show "monic V'"
[PROOF STATE]
proof (prove)
using this:
monic v
lead_coeff V' = @lead_coeff v

goal (1 subgoal):
 1. monic V'
[PROOF STEP]
by (simp add:)
[PROOF STATE]
proof (state)
this:
monic V'

goal (4 subgoals):
 1. v = #V'
 2. w = #W'
 3. comm_monoid_mult_class.coprime (#V') (#W')
 4. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from vV
[PROOF STATE]
proof (chain)
picking this:
v = #(#v + Polynomial.smult (of_nat q) (#v'))
[PROOF STEP]
show "v = #V'"
[PROOF STATE]
proof (prove)
using this:
v = #(#v + Polynomial.smult (of_nat q) (#v'))

goal (1 subgoal):
 1. v = #V'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v = #V'

goal (3 subgoals):
 1. w = #W'
 2. comm_monoid_mult_class.coprime (#V') (#W')
 3. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from wW
[PROOF STATE]
proof (chain)
picking this:
w = #(#w + Polynomial.smult (of_nat q) (#w'))
[PROOF STEP]
show "w = #W'"
[PROOF STATE]
proof (prove)
using this:
w = #(#w + Polynomial.smult (of_nat q) (#w'))

goal (1 subgoal):
 1. w = #W'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w = #W'

goal (2 subgoals):
 1. comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
from coprime_preserves
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime (#(#v + Polynomial.smult (of_nat q) (#v'))) (#(#w + Polynomial.smult (of_nat q) (#w')))
[PROOF STEP]
show "coprime (#V' :: 'p mod_ring poly) (#W')"
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime (#(#v + Polynomial.smult (of_nat q) (#v'))) (#(#w + Polynomial.smult (of_nat q) (#w')))

goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (#V') (#W')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
comm_monoid_mult_class.coprime (#V') (#W')

goal (1 subgoal):
 1. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
show 9: ?unique
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
by (unfold 1, intro allI conjI impI; rule unique)
[PROOF STATE]
proof (state)
this:
\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')

goal (2 subgoals):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
 2. \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')
[PROOF STEP]
show ?main ?unique
[PROOF STATE]
proof (prove)
using this:
(u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')) \<and> (\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W')

goal (1 subgoal):
 1. u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W') &&& \<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'
[PROOF STEP]
by (fact conjunct1, fact conjunct2)
[PROOF STATE]
proof (state)
this:
u = V' * W' \<and> v = #V' \<and> w = #W' \<and> degree V' = degree v \<and> degree W' = degree w \<and> monic V' \<and> comm_monoid_mult_class.coprime (#V') (#W')
\<forall>V'' W''. u = V'' * W'' \<longrightarrow> v = #V'' \<longrightarrow> w = #W'' \<longrightarrow> degree V'' = degree v \<longrightarrow> degree W'' = degree w \<longrightarrow> lead_coeff V'' = @lead_coeff v \<longrightarrow> V'' = V' \<and> W'' = W'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma discover_simps[simp]:
    "counter (discover u v s) = Suc (counter s)"
    "discovered (discover u v s) = (discovered s)(v \<mapsto> counter s)"
    "finished (discover u v s) = finished s"
    "stack (discover u v s) = v#stack s"
    "pending (discover u v s) = pending s \<union> {v} \<times> E``{v}"
    "tree_edges (discover u v s) = insert (u,v) (tree_edges s)"
    "cross_edges (discover u v s) = cross_edges s"
    "back_edges (discover u v s) = back_edges s"
    "state.more (discover u v s) = state.more s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((counter (discover u v s) = Suc (counter s) &&& discovered (discover u v s) = discovered s(v \<mapsto> counter s)) &&& finished (discover u v s) = finished s &&& stack (discover u v s) = v # stack s) &&& (pending (discover u v s) = pending s \<union> {v} \<times> E `` {v} &&& tree_edges (discover u v s) = insert (u, v) (tree_edges s)) &&& cross_edges (discover u v s) = cross_edges s &&& back_edges (discover u v s) = back_edges s &&& state.more (discover u v s) = state.more s
[PROOF STEP]
by (simp_all add: discover_def)


[STATEMENT]
lemma finish_simps[simp]:
    "counter (finish u s) = Suc (counter s)"
    "discovered (finish u s) = discovered s"
    "finished (finish u s) = (finished s)(u \<mapsto> counter s)"
    "stack (finish u s) = tl (stack s)"
    "pending (finish u s) = pending s"
    "tree_edges (finish u s) = tree_edges s"
    "cross_edges (finish u s) = cross_edges s"
    "back_edges (finish u s) = back_edges s"
    "state.more (finish u s) = state.more s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((counter (finish u s) = Suc (counter s) &&& discovered (finish u s) = discovered s) &&& finished (finish u s) = finished s(u \<mapsto> counter s) &&& stack (finish u s) = tl (stack s)) &&& (pending (finish u s) = pending s &&& tree_edges (finish u s) = tree_edges s) &&& cross_edges (finish u s) = cross_edges s &&& back_edges (finish u s) = back_edges s &&& state.more (finish u s) = state.more s
[PROOF STEP]
by (simp_all add: finish_def)


[STATEMENT]
lemma back_edge_simps[simp]:
    "counter (back_edge u v s) = counter s"
    "discovered (back_edge u v s) = discovered s"
    "finished (back_edge u v s) = finished s"
    "stack (back_edge u v s) = stack s"
    "pending (back_edge u v s) = pending s"
    "tree_edges (back_edge u v s) = tree_edges s"
    "cross_edges (back_edge u v s) = cross_edges s"
    "back_edges (back_edge u v s) = insert (u,v) (back_edges s)"
    "state.more (back_edge u v s) = state.more s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((counter (back_edge u v s) = counter s &&& discovered (back_edge u v s) = discovered s) &&& finished (back_edge u v s) = finished s &&& stack (back_edge u v s) = stack s) &&& (pending (back_edge u v s) = pending s &&& tree_edges (back_edge u v s) = tree_edges s) &&& cross_edges (back_edge u v s) = cross_edges s &&& back_edges (back_edge u v s) = insert (u, v) (back_edges s) &&& state.more (back_edge u v s) = state.more s
[PROOF STEP]
by (simp_all add: back_edge_def)


[STATEMENT]
lemma cross_edge_simps[simp]:
    "counter (cross_edge u v s) = counter s"
    "discovered (cross_edge u v s) = discovered s"
    "finished (cross_edge u v s) = finished s"
    "stack (cross_edge u v s) = stack s"
    "pending (cross_edge u v s) = pending s"
    "tree_edges (cross_edge u v s) = tree_edges s"
    "cross_edges (cross_edge u v s) = insert (u,v) (cross_edges s)"
    "back_edges (cross_edge u v s) = back_edges s"
    "state.more (cross_edge u v s) = state.more s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((counter (cross_edge u v s) = counter s &&& discovered (cross_edge u v s) = discovered s) &&& finished (cross_edge u v s) = finished s &&& stack (cross_edge u v s) = stack s) &&& (pending (cross_edge u v s) = pending s &&& tree_edges (cross_edge u v s) = tree_edges s) &&& cross_edges (cross_edge u v s) = insert (u, v) (cross_edges s) &&& back_edges (cross_edge u v s) = back_edges s &&& state.more (cross_edge u v s) = state.more s
[PROOF STEP]
by (simp_all add: cross_edge_def)


[STATEMENT]
lemma new_root_simps[simp]:
    "counter (new_root v0 s) = Suc (counter s)"
    "discovered (new_root v0 s) = (discovered s)(v0 \<mapsto> counter s)"
    "finished (new_root v0 s) = finished s"
    "stack (new_root v0 s) = [v0]"
    "pending (new_root v0 s) = ({v0}\<times>E``{v0})"
    "tree_edges (new_root v0 s) = tree_edges s"
    "cross_edges (new_root v0 s) = cross_edges s"
    "back_edges (new_root v0 s) = back_edges s"
    "state.more (new_root v0 s) = state.more s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((counter (new_root v0 s) = Suc (counter s) &&& discovered (new_root v0 s) = discovered s(v0 \<mapsto> counter s)) &&& finished (new_root v0 s) = finished s &&& stack (new_root v0 s) = [v0]) &&& (pending (new_root v0 s) = {v0} \<times> E `` {v0} &&& tree_edges (new_root v0 s) = tree_edges s) &&& cross_edges (new_root v0 s) = cross_edges s &&& back_edges (new_root v0 s) = back_edges s &&& state.more (new_root v0 s) = state.more s
[PROOF STEP]
by (simp_all add: new_root_def)


[STATEMENT]
lemma empty_state_simps[simp]:
    "counter (empty_state e) = 0"
    "discovered (empty_state e) = Map.empty"
    "finished (empty_state e) = Map.empty"
    "pending (empty_state e) = {}"
    "stack (empty_state e) = []"
    "tree_edges (empty_state e) = {}"
    "back_edges (empty_state e) = {}"
    "cross_edges (empty_state e) = {}"
    "state.more (empty_state e) = e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((counter (empty_state e) = 0 &&& discovered (empty_state e) = Map.empty) &&& finished (empty_state e) = Map.empty &&& pending (empty_state e) = {}) &&& (stack (empty_state e) = [] &&& tree_edges (empty_state e) = {}) &&& back_edges (empty_state e) = {} &&& cross_edges (empty_state e) = {} &&& state.more (empty_state e) = e
[PROOF STEP]
by (simp_all add: empty_state_def)


[STATEMENT]
lemma cond_alt:
    "cond = (\<lambda>s. (V0 \<subseteq> dom (discovered s) \<longrightarrow> stack s \<noteq> []) \<and> \<not>is_break param s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cond = (\<lambda>s. (V0 \<subseteq> dom (discovered s) \<longrightarrow> stack s \<noteq> []) \<and> \<not> is_break param s)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. cond s = ((V0 \<subseteq> dom (discovered s) \<longrightarrow> stack s \<noteq> []) \<and> \<not> is_break param s)
[PROOF STEP]
unfolding cond_def is_discovered_def is_empty_stack_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. ((V0 \<subseteq> {v. v \<in> dom (discovered s)} \<longrightarrow> stack s \<noteq> []) \<and> \<not> is_break param s) = ((V0 \<subseteq> dom (discovered s) \<longrightarrow> stack s \<noteq> []) \<and> \<not> is_break param s)
[PROOF STEP]
by auto


[STATEMENT]
lemma make_invar_thm: "is_invar I \<Longrightarrow> I s"
    \<comment> \<open>Lemma to transfer an invariant into this locale\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar I \<Longrightarrow> I s
[PROOF STEP]
using rwof_cons[OF _ rwof, folded is_invar_def]
[PROOF STATE]
proof (prove)
using this:
is_invar ?I \<Longrightarrow> ?I s

goal (1 subgoal):
 1. is_invar I \<Longrightarrow> I s
[PROOF STEP]
.


[STATEMENT]
lemma rwof_eq_DFS_invar[simp]:
    "rwof init cond step = DFS_invar G param"
    \<comment> \<open>The DFS-invar locale is equivalent to the strongest invariant of the loop.\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rwof init cond step = DFS_invar G param
[PROOF STEP]
apply (auto intro: DFS_invar.rwof intro!: ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. rwof init cond step x \<Longrightarrow> DFS_invar G param x
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma DFS_invar_step: "\<lbrakk>nofail it_dfs; DFS_invar G param s; cond s\<rbrakk>
    \<Longrightarrow> step s \<le> SPEC (DFS_invar G param)"
    \<comment> \<open>A step preserves the (best) invariant.\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nofail it_dfs; DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (DFS_invar G param)
[PROOF STEP]
unfolding it_dfs_def rwof_eq_DFS_invar[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nofail (init \<bind> WHILE cond step); rwof init cond step s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (rwof init cond step)
[PROOF STEP]
by (rule rwof_step)


[STATEMENT]
lemma DFS_invar_step': "\<lbrakk>nofail (step s); DFS_invar G param s; cond s\<rbrakk>
    \<Longrightarrow> step s \<le> SPEC (DFS_invar G param)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nofail (step s); DFS_invar G param s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (DFS_invar G param)
[PROOF STEP]
unfolding it_dfs_def rwof_eq_DFS_invar[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nofail (step s); rwof init cond step s; cond s\<rbrakk> \<Longrightarrow> step s \<le> SPEC (rwof init cond step)
[PROOF STEP]
by (rule rwof_step')


[STATEMENT]
lemma establish_invarI[case_names init new_root finish cross_edge back_edge discover]:
    \<comment> \<open>Establish a DFS invariant (explicit preconditions).\<close>
    assumes init: "on_init param \<le>\<^sub>n SPEC (\<lambda>x. I (empty_state x))"
    assumes new_root: "\<And>s s' v0.
      \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
       stack s = []; v0 \<in> V0; v0 \<notin> dom (discovered s);
        s' = new_root v0 s\<rbrakk>
         \<Longrightarrow> on_new_root param v0 s' \<le>\<^sub>n
             SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                         \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes finish: "\<And>s s' u.
      \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
       stack s \<noteq> []; u = hd (stack s);
       pending s `` {u} = {};
       s' = finish u s\<rbrakk>
         \<Longrightarrow> on_finish param u s' \<le>\<^sub>n
              SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                        \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes cross_edge: "\<And>s s' u v.
       \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
        stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s);
        v \<in> dom (discovered s); v\<in>dom (finished s);
        s' = cross_edge u v (s\<lparr>pending := pending s - {(u,v)}\<rparr>)\<rbrakk>
       \<Longrightarrow> on_cross_edge param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes back_edge: "\<And>s s' u v.
       \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
        stack s \<noteq> []; (u, v) \<in> pending s; u = hd (stack s);
        v \<in> dom (discovered s); v\<notin>dom (finished s);
        s' = back_edge u v (s\<lparr>pending := pending s - {(u,v)}\<rparr>)\<rbrakk>
       \<Longrightarrow> on_back_edge param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    assumes discover: "\<And>s s' u v.
       \<lbrakk>DFS_invar G param s; I s; cond s; \<not> is_break param s;
        stack s \<noteq> [];  (u, v) \<in> pending s; u = hd (stack s);
        v \<notin> dom (discovered s);
        s' = discover u v (s\<lparr>pending := pending s - {(u,v)}\<rparr>)\<rbrakk>
       \<Longrightarrow> on_discover param u v s' \<le>\<^sub>n
           SPEC (\<lambda>x. DFS_invar G param (s'\<lparr>state.more := x\<rparr>)
                      \<longrightarrow> I (s'\<lparr>state.more := x\<rparr>))"
    shows "is_invar I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_invar I
[PROOF STEP]
unfolding is_invar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_rwof_invar init cond step I
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. init \<le>\<^sub>n SPEC I
 2. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
show "init \<le>\<^sub>n SPEC I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<le>\<^sub>n SPEC I
[PROOF STEP]
unfolding init_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_init param \<bind> (\<lambda>e. RETURN (empty_state e)) \<le>\<^sub>n SPEC I
[PROOF STEP]
by (refine_rcg refine_vcg) (simp add: init)
[PROOF STATE]
proof (state)
this:
init \<le>\<^sub>n SPEC I

goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
assume "rwof init cond step s" and IC: "I s" "cond s"
[PROOF STATE]
proof (state)
this:
rwof init cond step s
I s
cond s

goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
hence DI: "DFS_invar G param s"
[PROOF STATE]
proof (prove)
using this:
rwof init cond step s
I s
cond s

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
DFS_invar G param s

goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
DFS_invar G param s
[PROOF STEP]
interpret DFS_invar G param s
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s

goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
from \<open>cond s\<close>
[PROOF STATE]
proof (chain)
picking this:
cond s
[PROOF STEP]
have IB: "\<not> is_break param s"
[PROOF STATE]
proof (prove)
using this:
cond s

goal (1 subgoal):
 1. \<not> is_break param s
[PROOF STEP]
by (simp add: cond_def)
[PROOF STATE]
proof (state)
this:
\<not> is_break param s

goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
have B: "step s \<le>\<^sub>n SPEC (DFS_invar G param)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step s \<le>\<^sub>n SPEC (DFS_invar G param)
[PROOF STEP]
by rule (metis DFS_invar_step' DI \<open>cond s\<close>)
[PROOF STATE]
proof (state)
this:
step s \<le>\<^sub>n SPEC (DFS_invar G param)

goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
note rule_assms = DI IC IB
[PROOF STATE]
proof (state)
this:
DFS_invar G param s
I s
cond s
\<not> is_break param s

goal (1 subgoal):
 1. \<And>s. \<lbrakk>rwof init cond step s; I s; cond s\<rbrakk> \<Longrightarrow> step s \<le>\<^sub>n SPEC I
[PROOF STEP]
show "step s \<le>\<^sub>n SPEC I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step s \<le>\<^sub>n SPEC I
[PROOF STEP]
apply (rule leof_use_spec_rule[OF B])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step s \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s)
[PROOF STEP]
unfolding step_def do_defs pred_defs get_pending_def get_new_root_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if stack s = [] then SPEC (\<lambda>v. v \<in> V0 \<and> v \<notin> dom (discovered s)) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if v \<in> dom (discovered s) then if v \<in> dom (finished s) then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s)
[PROOF STEP]
apply (refine_rcg refine_vcg)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>stack s = []; x \<in> {v \<in> V0. v \<notin> dom (discovered s)}\<rbrakk> \<Longrightarrow> on_new_root param x (new_root x s) \<le>\<^sub>n SPEC (\<lambda>xa. RETURN (new_root x s\<lparr>state.more := xa\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
 2. \<And>x1 x2 x1a x2a. \<lbrakk>stack s \<noteq> []; pending s `` {hd (stack s)} = {}; x2 = (x1a, x2a); (hd (stack s), None, s) = (x1, x2); x1a = None\<rbrakk> \<Longrightarrow> on_finish param x1 (finish x1 x2a) \<le>\<^sub>n SPEC (\<lambda>x. RETURN (finish x1 x2a\<lparr>state.more := x\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
 3. \<And>x1 x2 x1a x2a v. \<lbrakk>stack s \<noteq> []; pending s `` {hd (stack s)} = {}; x2 = (x1a, x2a); (hd (stack s), None, s) = (x1, x2); x1a = Some v; v \<in> dom (discovered x2a); v \<in> dom (finished x2a)\<rbrakk> \<Longrightarrow> on_cross_edge param x1 v (cross_edge x1 v x2a) \<le>\<^sub>n SPEC (\<lambda>x. RETURN (cross_edge x1 v x2a\<lparr>state.more := x\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
 4. \<And>x1 x2 x1a x2a v. \<lbrakk>stack s \<noteq> []; pending s `` {hd (stack s)} = {}; x2 = (x1a, x2a); (hd (stack s), None, s) = (x1, x2); x1a = Some v; v \<in> dom (discovered x2a); v \<notin> dom (finished x2a)\<rbrakk> \<Longrightarrow> on_back_edge param x1 v (back_edge x1 v x2a) \<le>\<^sub>n SPEC (\<lambda>x. RETURN (back_edge x1 v x2a\<lparr>state.more := x\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
 5. \<And>x1 x2 x1a x2a v. \<lbrakk>stack s \<noteq> []; pending s `` {hd (stack s)} = {}; x2 = (x1a, x2a); (hd (stack s), None, s) = (x1, x2); x1a = Some v; v \<notin> dom (discovered x2a)\<rbrakk> \<Longrightarrow> on_discover param x1 v (discover x1 v x2a) \<le>\<^sub>n SPEC (\<lambda>x. RETURN (discover x1 v x2a\<lparr>state.more := x\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
 6. \<And>x x1 x2 x1a x2a. \<lbrakk>stack s \<noteq> []; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; x2 = (x1a, x2a); (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (x1, x2); x1a = None\<rbrakk> \<Longrightarrow> on_finish param x1 (finish x1 x2a) \<le>\<^sub>n SPEC (\<lambda>x. RETURN (finish x1 x2a\<lparr>state.more := x\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
 7. \<And>x x1 x2 x1a x2a v. \<lbrakk>stack s \<noteq> []; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; x2 = (x1a, x2a); (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (x1, x2); x1a = Some v; v \<in> dom (discovered x2a); v \<in> dom (finished x2a)\<rbrakk> \<Longrightarrow> on_cross_edge param x1 v (cross_edge x1 v x2a) \<le>\<^sub>n SPEC (\<lambda>x. RETURN (cross_edge x1 v x2a\<lparr>state.more := x\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
 8. \<And>x x1 x2 x1a x2a v. \<lbrakk>stack s \<noteq> []; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; x2 = (x1a, x2a); (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (x1, x2); x1a = Some v; v \<in> dom (discovered x2a); v \<notin> dom (finished x2a)\<rbrakk> \<Longrightarrow> on_back_edge param x1 v (back_edge x1 v x2a) \<le>\<^sub>n SPEC (\<lambda>x. RETURN (back_edge x1 v x2a\<lparr>state.more := x\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
 9. \<And>x x1 x2 x1a x2a v. \<lbrakk>stack s \<noteq> []; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; x2 = (x1a, x2a); (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (x1, x2); x1a = Some v; v \<notin> dom (discovered x2a)\<rbrakk> \<Longrightarrow> on_discover param x1 v (discover x1 v x2a) \<le>\<^sub>n SPEC (\<lambda>x. RETURN (discover x1 v x2a\<lparr>state.more := x\<rparr>) \<le>\<^sub>n SPEC (\<lambda>s. DFS_invar G param s \<longrightarrow> I s))
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>stack s = []; x \<in> V0 \<and> x \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> on_new_root param x (new_root x s) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (new_root x s\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (new_root x s\<lparr>state.more := xa\<rparr>))
 2. \<And>x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} = {}; x2 = (None, s); hd (stack s) = x1; x1a = None\<rbrakk> \<Longrightarrow> on_finish param x1 (finish x1 s) \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (finish x1 s\<lparr>state.more := x\<rparr>) \<longrightarrow> I (finish x1 s\<lparr>state.more := x\<rparr>))
 3. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<in> dom (discovered s); x \<in> dom (finished s)\<rbrakk> \<Longrightarrow> on_cross_edge param x1 x (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
 4. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<in> dom (discovered s); x \<notin> dom (finished s)\<rbrakk> \<Longrightarrow> on_back_edge param x1 x (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
 5. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> on_discover param x1 x (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
[PROOF STEP]
apply (blast intro: new_root[OF rule_assms])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} = {}; x2 = (None, s); hd (stack s) = x1; x1a = None\<rbrakk> \<Longrightarrow> on_finish param x1 (finish x1 s) \<le>\<^sub>n SPEC (\<lambda>x. DFS_invar G param (finish x1 s\<lparr>state.more := x\<rparr>) \<longrightarrow> I (finish x1 s\<lparr>state.more := x\<rparr>))
 2. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<in> dom (discovered s); x \<in> dom (finished s)\<rbrakk> \<Longrightarrow> on_cross_edge param x1 x (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
 3. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<in> dom (discovered s); x \<notin> dom (finished s)\<rbrakk> \<Longrightarrow> on_back_edge param x1 x (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
 4. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> on_discover param x1 x (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
[PROOF STEP]
apply (blast intro: finish[OF rule_assms])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<in> dom (discovered s); x \<in> dom (finished s)\<rbrakk> \<Longrightarrow> on_cross_edge param x1 x (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (cross_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
 2. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<in> dom (discovered s); x \<notin> dom (finished s)\<rbrakk> \<Longrightarrow> on_back_edge param x1 x (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
 3. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> on_discover param x1 x (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
[PROOF STEP]
apply (rule cross_edge[OF rule_assms], auto) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<in> dom (discovered s); x \<notin> dom (finished s)\<rbrakk> \<Longrightarrow> on_back_edge param x1 x (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (back_edge x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
 2. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> on_discover param x1 x (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
[PROOF STEP]
apply (rule back_edge[OF rule_assms], auto) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2 x1a. \<lbrakk>stack s \<noteq> []; pending s `` {x1} \<noteq> {}; (x1, x) \<in> pending s; x2 = (Some x, s\<lparr>pending := pending s - {(x1, x)}\<rparr>); hd (stack s) = x1; x1a = Some x; x \<notin> dom (discovered s)\<rbrakk> \<Longrightarrow> on_discover param x1 x (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)) \<le>\<^sub>n SPEC (\<lambda>xa. DFS_invar G param (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>) \<longrightarrow> I (discover x1 x (s\<lparr>pending := pending s - {(x1, x)}\<rparr>)\<lparr>state.more := xa\<rparr>))
[PROOF STEP]
apply (rule discover[OF rule_assms], auto) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
step s \<le>\<^sub>n SPEC I

goal:
No subgoals!
[PROOF STEP]
qed