[STATEMENT]
lemma product_from_reachable_path' :
  assumes "path (product (from_FSM M q1) (from_FSM M q2)) (q1', q2') p"
  and     "q1 \<in> reachable_states M"
  and     "q2 \<in> reachable_states M"
shows "path (product (from_FSM M q1') (from_FSM M q2')) (q1', q2') p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Product_FSM.product (from_FSM M q1') (from_FSM M q2')) (q1', q2') p
[PROOF STEP]
by (meson assms(1) assms(2) assms(3) from_FSM_path from_FSM_path_rev_initial product_path reachable_state_is_state)


[STATEMENT]
lemma product_from :
  assumes "q1 \<in> states M"
  and     "q2 \<in> states M"
shows "product (from_FSM M q1) (from_FSM M q2) = from_FSM (product M M) (q1,q2)" (is "?PF = ?FP")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Product_FSM.product (from_FSM M q1) (from_FSM M q2) = from_FSM (Product_FSM.product M M) (q1, q2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Product_FSM.product (from_FSM M q1) (from_FSM M q2) = from_FSM (Product_FSM.product M M) (q1, q2)
[PROOF STEP]
have "(q1,q2) \<in> states (product M M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q1, q2) \<in> FSM.states (Product_FSM.product M M)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. (q1, q2) \<in> FSM.states (Product_FSM.product M M)
[PROOF STEP]
unfolding product_simps
[PROOF STATE]
proof (prove)
using this:
q1 \<in> FSM.states M
q2 \<in> FSM.states M

goal (1 subgoal):
 1. (q1, q2) \<in> FSM.states M \<times> FSM.states M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q1, q2) \<in> FSM.states (Product_FSM.product M M)

goal (1 subgoal):
 1. Product_FSM.product (from_FSM M q1) (from_FSM M q2) = from_FSM (Product_FSM.product M M) (q1, q2)
[PROOF STEP]
have "initial ?FP = initial ?PF"
  and  "inputs ?FP = inputs ?PF"
  and  "outputs ?FP = outputs ?PF"
  and  "states ?FP = states ?PF"
  and  "transitions ?FP = transitions ?PF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FSM.initial (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) &&& FSM.inputs (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))) &&& FSM.outputs (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.outputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) &&& FSM.states (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.states (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) &&& FSM.transitions (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
unfolding product_simps
              from_FSM_simps[OF assms(1)]
              from_FSM_simps[OF assms(2)]
              from_FSM_simps[OF \<open>(q1,q2) \<in> states (product M M)\<close>]
              product_transitions_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((q1, q2) = (q1, q2) &&& FSM.inputs M \<union> FSM.inputs M = FSM.inputs M \<union> FSM.inputs M) &&& FSM.outputs M \<union> FSM.outputs M = FSM.outputs M \<union> FSM.outputs M &&& FSM.states M \<times> FSM.states M = FSM.states M \<times> FSM.states M &&& {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions M \<and> (qB, x, y, qB') \<in> FSM.transitions M} = {((qA, qB), x, y, qA', qB') |qA qB x y qA' qB'. (qA, x, y, qA') \<in> FSM.transitions M \<and> (qB, x, y, qB') \<in> FSM.transitions M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
FSM.initial (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.inputs (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.outputs (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.outputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.states (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.states (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.transitions (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. Product_FSM.product (from_FSM M q1) (from_FSM M q2) = from_FSM (Product_FSM.product M M) (q1, q2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.initial (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.inputs (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.outputs (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.outputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.states (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.states (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.transitions (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FSM.initial (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.inputs (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.inputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.outputs (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.outputs (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.states (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.states (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
FSM.transitions (from_FSM (Product_FSM.product M M) (q1, q2)) = FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. Product_FSM.product (from_FSM M q1) (from_FSM M q2) = from_FSM (Product_FSM.product M M) (q1, q2)
[PROOF STEP]
by (transfer; auto)
[PROOF STATE]
proof (state)
this:
Product_FSM.product (from_FSM M q1) (from_FSM M q2) = from_FSM (Product_FSM.product M M) (q1, q2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma product_from_from :
  assumes "(q1',q2') \<in> states (product (from_FSM M q1) (from_FSM M q2))"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
shows "(product (from_FSM M q1') (from_FSM M q2')) = (from_FSM (product (from_FSM M q1) (from_FSM M q2)) (q1',q2'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Product_FSM.product (from_FSM M q1') (from_FSM M q2') = from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')
[PROOF STEP]
using product_from
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q1.0 \<in> FSM.states ?M; ?q2.0 \<in> FSM.states ?M\<rbrakk> \<Longrightarrow> Product_FSM.product (from_FSM ?M ?q1.0) (from_FSM ?M ?q2.0) = from_FSM (Product_FSM.product ?M ?M) (?q1.0, ?q2.0)

goal (1 subgoal):
 1. Product_FSM.product (from_FSM M q1') (from_FSM M q2') = from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2')
[PROOF STEP]
by (metis (no_types, lifting) assms(1) assms(2) assms(3) from_FSM_simps(5) from_from mem_Sigma_iff product_simps(2))


[STATEMENT]
lemma submachine_transition_product_from :
  assumes "is_submachine S (product (from_FSM M q1) (from_FSM M q2))"
  and     "((q1,q2),x,y,(q1',q2')) \<in> transitions S"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
 shows "is_submachine (from_FSM S (q1',q2')) (product (from_FSM M q1') (from_FSM M q2'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_submachine (from_FSM S (q1', q2')) (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_submachine (from_FSM S (q1', q2')) (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
have "((q1,q2),x,y,(q1',q2')) \<in> transitions (product (from_FSM M q1) (from_FSM M q2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((q1, q2), x, y, q1', q2') \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
using assms(1) assms(2)
[PROOF STATE]
proof (prove)
using this:
is_submachine S (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
((q1, q2), x, y, q1', q2') \<in> FSM.transitions S

goal (1 subgoal):
 1. ((q1, q2), x, y, q1', q2') \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((q1, q2), x, y, q1', q2') \<in> FSM.transitions (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. is_submachine (from_FSM S (q1', q2')) (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
have "(q1',q2') \<in> states S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q1', q2') \<in> FSM.states S
[PROOF STEP]
using fsm_transition_target assms(2)
[PROOF STATE]
proof (prove)
using this:
?t \<in> FSM.transitions ?M \<Longrightarrow> t_target ?t \<in> FSM.states ?M
((q1, q2), x, y, q1', q2') \<in> FSM.transitions S

goal (1 subgoal):
 1. (q1', q2') \<in> FSM.states S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q1', q2') \<in> FSM.states S

goal (1 subgoal):
 1. is_submachine (from_FSM S (q1', q2')) (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_submachine (from_FSM S (q1', q2')) (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
using product_from_reachable_next[OF \<open>((q1,q2),x,y,(q1',q2')) \<in> transitions (product (from_FSM M q1) (from_FSM M q2))\<close> assms(3,4)]
          submachine_from[OF assms(1) \<open>(q1',q2') \<in> states S\<close>]
[PROOF STATE]
proof (prove)
using this:
from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2') = Product_FSM.product (from_FSM M q1') (from_FSM M q2')
is_submachine (from_FSM S (q1', q2')) (from_FSM (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) (q1', q2'))

goal (1 subgoal):
 1. is_submachine (from_FSM S (q1', q2')) (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_submachine (from_FSM S (q1', q2')) (Product_FSM.product (from_FSM M q1') (from_FSM M q2'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma submachine_transition_complete_product_from :
  assumes "is_submachine S (product (from_FSM M q1) (from_FSM M q2))"
      and "completely_specified S"
      and "((q1,q2),x,y,(q1',q2')) \<in> transitions S"
  and     "q1 \<in> states M"
  and     "q2 \<in> states M"
 shows "completely_specified (from_FSM S (q1',q2'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
let ?P = "(product (from_FSM M q1) (from_FSM M q2))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
let ?P' = "(product (from_FSM M q1') (from_FSM M q2'))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
let ?F = "(from_FSM S (q1',q2'))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
have "initial ?P = (q1,q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = (q1, q2)
[PROOF STEP]
by (simp add: assms(4) assms(5) reachable_state_is_state)
[PROOF STATE]
proof (state)
this:
FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = (q1, q2)

goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = (q1, q2)
[PROOF STEP]
have "initial S = (q1,q2)"
[PROOF STATE]
proof (prove)
using this:
FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = (q1, q2)

goal (1 subgoal):
 1. FSM.initial S = (q1, q2)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
FSM.initial (Product_FSM.product (from_FSM M q1) (from_FSM M q2)) = (q1, q2)
is_submachine S (Product_FSM.product (from_FSM M q1) (from_FSM M q2))

goal (1 subgoal):
 1. FSM.initial S = (q1, q2)
[PROOF STEP]
by (metis is_submachine.simps)
[PROOF STATE]
proof (state)
this:
FSM.initial S = (q1, q2)

goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
FSM.initial S = (q1, q2)
[PROOF STEP]
have "(q1',q2') \<in> states S"
[PROOF STATE]
proof (prove)
using this:
FSM.initial S = (q1, q2)

goal (1 subgoal):
 1. (q1', q2') \<in> FSM.states S
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
FSM.initial S = (q1, q2)
((q1, q2), x, y, q1', q2') \<in> FSM.transitions S

goal (1 subgoal):
 1. (q1', q2') \<in> FSM.states S
[PROOF STEP]
using fsm_transition_target
[PROOF STATE]
proof (prove)
using this:
FSM.initial S = (q1, q2)
((q1, q2), x, y, q1', q2') \<in> FSM.transitions S
?t \<in> FSM.transitions ?M \<Longrightarrow> t_target ?t \<in> FSM.states ?M

goal (1 subgoal):
 1. (q1', q2') \<in> FSM.states S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(q1', q2') \<in> FSM.states S

goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q1', q2') \<in> FSM.states S
[PROOF STEP]
have "states ?F = states S"
[PROOF STATE]
proof (prove)
using this:
(q1', q2') \<in> FSM.states S

goal (1 subgoal):
 1. FSM.states (from_FSM S (q1', q2')) = FSM.states S
[PROOF STEP]
using from_FSM_simps(5)
[PROOF STATE]
proof (prove)
using this:
(q1', q2') \<in> FSM.states S
?q \<in> FSM.states ?M \<Longrightarrow> FSM.states (from_FSM ?M ?q) = FSM.states ?M

goal (1 subgoal):
 1. FSM.states (from_FSM S (q1', q2')) = FSM.states S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
FSM.states (from_FSM S (q1', q2')) = FSM.states S

goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
FSM.states (from_FSM S (q1', q2')) = FSM.states S

goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
have "inputs ?F = inputs S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.inputs (from_FSM S (q1', q2')) = FSM.inputs S
[PROOF STEP]
using from_FSM_simps(2) \<open>(q1',q2') \<in> states S\<close>
[PROOF STATE]
proof (prove)
using this:
?q \<in> FSM.states ?M \<Longrightarrow> FSM.inputs (from_FSM ?M ?q) = FSM.inputs ?M
(q1', q2') \<in> FSM.states S

goal (1 subgoal):
 1. FSM.inputs (from_FSM S (q1', q2')) = FSM.inputs S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
FSM.inputs (from_FSM S (q1', q2')) = FSM.inputs S

goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
FSM.states (from_FSM S (q1', q2')) = FSM.states S
FSM.inputs (from_FSM S (q1', q2')) = FSM.inputs S
[PROOF STEP]
show "completely_specified ?F"
[PROOF STATE]
proof (prove)
using this:
FSM.states (from_FSM S (q1', q2')) = FSM.states S
FSM.inputs (from_FSM S (q1', q2')) = FSM.inputs S

goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
FSM.states (from_FSM S (q1', q2')) = FSM.states S
FSM.inputs (from_FSM S (q1', q2')) = FSM.inputs S
completely_specified S

goal (1 subgoal):
 1. completely_specified (from_FSM S (q1', q2'))
[PROOF STEP]
unfolding completely_specified.simps
[PROOF STATE]
proof (prove)
using this:
FSM.states (from_FSM S (q1', q2')) = FSM.states S
FSM.inputs (from_FSM S (q1', q2')) = FSM.inputs S
\<forall>q\<in>FSM.states S. \<forall>x\<in>FSM.inputs S. \<exists>t\<in>FSM.transitions S. t_source t = q \<and> t_input t = x

goal (1 subgoal):
 1. \<forall>q\<in>FSM.states (from_FSM S (q1', q2')). \<forall>x\<in>FSM.inputs (from_FSM S (q1', q2')). \<exists>t\<in>FSM.transitions (from_FSM S (q1', q2')). t_source t = q \<and> t_input t = x
[PROOF STEP]
by (meson assms(2) completely_specified.elims(2) from_FSM_completely_specified)
[PROOF STATE]
proof (state)
this:
completely_specified (from_FSM S (q1', q2'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_product :
  assumes "acyclic B"
  shows "acyclic (product A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.acyclic (Product_FSM.product A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FSM.acyclic (Product_FSM.product A B)
[PROOF STEP]
show "acyclic (product A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FSM.acyclic (Product_FSM.product A B)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> FSM.acyclic (Product_FSM.product A B) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> FSM.acyclic (Product_FSM.product A B)"
[PROOF STATE]
proof (state)
this:
\<not> FSM.acyclic (Product_FSM.product A B)

goal (1 subgoal):
 1. \<not> FSM.acyclic (Product_FSM.product A B) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> FSM.acyclic (Product_FSM.product A B)
[PROOF STEP]
obtain p where "path (product A B) (initial (product A B)) p" and "\<not> distinct (visited_states (initial (product A B)) p)"
[PROOF STATE]
proof (prove)
using this:
\<not> FSM.acyclic (Product_FSM.product A B)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p; \<not> distinct (visited_states (FSM.initial (Product_FSM.product A B)) p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p
\<not> distinct (visited_states (FSM.initial (Product_FSM.product A B)) p)

goal (1 subgoal):
 1. \<not> FSM.acyclic (Product_FSM.product A B) \<Longrightarrow> False
[PROOF STEP]
have "path B (initial B) (right_path p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path B (FSM.initial B) (right_path p)
[PROOF STEP]
using product_path[of A B] \<open>path (product A B) (initial (product A B)) p\<close>
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (?q1.0, ?q2.0) ?p = (path A ?q1.0 (left_path ?p) \<and> path B ?q2.0 (right_path ?p))
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p

goal (1 subgoal):
 1. path B (FSM.initial B) (right_path p)
[PROOF STEP]
unfolding product_simps
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (?q1.0, ?q2.0) ?p = (path A ?q1.0 (left_path ?p) \<and> path B ?q2.0 (right_path ?p))
path (Product_FSM.product A B) (FSM.initial A, FSM.initial B) p

goal (1 subgoal):
 1. path B (FSM.initial B) (right_path p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path B (FSM.initial B) (right_path p)

goal (1 subgoal):
 1. \<not> FSM.acyclic (Product_FSM.product A B) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
path B (FSM.initial B) (right_path p)

goal (1 subgoal):
 1. \<not> FSM.acyclic (Product_FSM.product A B) \<Longrightarrow> False
[PROOF STEP]
have "\<not> distinct (visited_states (initial B) (right_path p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
obtain i j where "i < j" and "j < length ((initial A, initial B) # map t_target p)" and "((initial A, initial B) # map t_target p) ! i = ((initial A, initial B) # map t_target p) ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; j < length ((FSM.initial A, FSM.initial B) # map t_target p); ((FSM.initial A, FSM.initial B) # map t_target p) ! i = ((FSM.initial A, FSM.initial B) # map t_target p) ! j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<not> distinct (visited_states (initial (product A B)) p)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> distinct (visited_states (FSM.initial (Product_FSM.product A B)) p)

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; j < length ((FSM.initial A, FSM.initial B) # map t_target p); ((FSM.initial A, FSM.initial B) # map t_target p) ! i = ((FSM.initial A, FSM.initial B) # map t_target p) ! j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding visited_states.simps product_simps
[PROOF STATE]
proof (prove)
using this:
\<not> distinct ((FSM.initial A, FSM.initial B) # map t_target p)

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; j < length ((FSM.initial A, FSM.initial B) # map t_target p); ((FSM.initial A, FSM.initial B) # map t_target p) ! i = ((FSM.initial A, FSM.initial B) # map t_target p) ! j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using non_distinct_repetition_indices
[PROOF STATE]
proof (prove)
using this:
\<not> distinct ((FSM.initial A, FSM.initial B) # map t_target p)
\<not> distinct ?xs \<Longrightarrow> \<exists>i j. i < j \<and> j < length ?xs \<and> ?xs ! i = ?xs ! j

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; j < length ((FSM.initial A, FSM.initial B) # map t_target p); ((FSM.initial A, FSM.initial B) # map t_target p) ! i = ((FSM.initial A, FSM.initial B) # map t_target p) ! j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i < j
j < length ((FSM.initial A, FSM.initial B) # map t_target p)
((FSM.initial A, FSM.initial B) # map t_target p) ! i = ((FSM.initial A, FSM.initial B) # map t_target p) ! j

goal (1 subgoal):
 1. \<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < j
j < length ((FSM.initial A, FSM.initial B) # map t_target p)
((FSM.initial A, FSM.initial B) # map t_target p) ! i = ((FSM.initial A, FSM.initial B) # map t_target p) ! j
[PROOF STEP]
have "snd (((initial A, initial B) # map t_target p) ! i) = snd (((initial A, initial B) # map t_target p) ! j)"
[PROOF STATE]
proof (prove)
using this:
i < j
j < length ((FSM.initial A, FSM.initial B) # map t_target p)
((FSM.initial A, FSM.initial B) # map t_target p) ! i = ((FSM.initial A, FSM.initial B) # map t_target p) ! j

goal (1 subgoal):
 1. snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i) = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i) = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! j)

goal (1 subgoal):
 1. \<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
have * :"i < length ((initial B) # map t_target (right_path p))"
      and  **:"j < length ((initial B) # map t_target (right_path p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (FSM.initial B # map t_target (right_path p)) &&& j < length (FSM.initial B # map t_target (right_path p))
[PROOF STEP]
using \<open>i < j\<close> \<open>j < length ((initial A, initial B) # map t_target p)\<close>
[PROOF STATE]
proof (prove)
using this:
i < j
j < length ((FSM.initial A, FSM.initial B) # map t_target p)

goal (1 subgoal):
 1. i < length (FSM.initial B # map t_target (right_path p)) &&& j < length (FSM.initial B # map t_target (right_path p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (FSM.initial B # map t_target (right_path p))
j < length (FSM.initial B # map t_target (right_path p))

goal (1 subgoal):
 1. \<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
have right_nth: "\<And> i . i < length ((initial B) # map t_target (right_path p)) \<Longrightarrow> ((initial B) # map t_target (right_path p)) ! i = snd (((initial A, initial B) # map t_target p) ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i)
[PROOF STEP]
have "((initial B) # map t_target (right_path p)) ! 0 = snd (((initial A, initial B) # map t_target p) ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FSM.initial B # map t_target (right_path p)) ! 0 = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(FSM.initial B # map t_target (right_path p)) ! 0 = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! 0)

goal (1 subgoal):
 1. \<And>i. i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(FSM.initial B # map t_target (right_path p)) ! 0 = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! 0)

goal (1 subgoal):
 1. \<And>i. i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i)
[PROOF STEP]
have "\<And> i . Suc i < length ((initial B) # map t_target (right_path p)) \<Longrightarrow> ((initial B) # map t_target (right_path p)) ! Suc i = snd (((initial A, initial B) # map t_target p) ! Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. Suc i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! Suc i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc ?i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! Suc ?i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! Suc ?i)

goal (1 subgoal):
 1. \<And>i. i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(FSM.initial B # map t_target (right_path p)) ! 0 = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! 0)
Suc ?i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! Suc ?i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! Suc ?i)
[PROOF STEP]
show "\<And> i . i < length ((initial B) # map t_target (right_path p)) \<Longrightarrow> ((initial B) # map t_target (right_path p)) ! i = snd (((initial A, initial B) # map t_target p) ! i)"
[PROOF STATE]
proof (prove)
using this:
(FSM.initial B # map t_target (right_path p)) ! 0 = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! 0)
Suc ?i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! Suc ?i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! Suc ?i)

goal (1 subgoal):
 1. \<And>i. i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i)
[PROOF STEP]
using less_Suc_eq_0_disj
[PROOF STATE]
proof (prove)
using this:
(FSM.initial B # map t_target (right_path p)) ! 0 = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! 0)
Suc ?i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! Suc ?i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! Suc ?i)
(?m < Suc ?n) = (?m = 0 \<or> (\<exists>j. ?m = Suc j \<and> j < ?n))

goal (1 subgoal):
 1. \<And>i. i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! ?i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! ?i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i < length (FSM.initial B # map t_target (right_path p)) \<Longrightarrow> (FSM.initial B # map t_target (right_path p)) ! ?i = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! ?i)

goal (1 subgoal):
 1. \<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
have "((initial B) # map t_target (right_path p)) ! i = ((initial B) # map t_target (right_path p)) ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (FSM.initial B # map t_target (right_path p)) ! i = (FSM.initial B # map t_target (right_path p)) ! j
[PROOF STEP]
using \<open>snd (((initial A, initial B) # map t_target p) ! i) = snd (((initial A, initial B) # map t_target p) ! j)\<close>
[PROOF STATE]
proof (prove)
using this:
snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i) = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! j)

goal (1 subgoal):
 1. (FSM.initial B # map t_target (right_path p)) ! i = (FSM.initial B # map t_target (right_path p)) ! j
[PROOF STEP]
unfolding right_nth[OF *] right_nth[OF **]
[PROOF STATE]
proof (prove)
using this:
snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i) = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! j)

goal (1 subgoal):
 1. snd (((FSM.initial A, FSM.initial B) # map t_target p) ! i) = snd (((FSM.initial A, FSM.initial B) # map t_target p) ! j)
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
(FSM.initial B # map t_target (right_path p)) ! i = (FSM.initial B # map t_target (right_path p)) ! j

goal (1 subgoal):
 1. \<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(FSM.initial B # map t_target (right_path p)) ! i = (FSM.initial B # map t_target (right_path p)) ! j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(FSM.initial B # map t_target (right_path p)) ! i = (FSM.initial B # map t_target (right_path p)) ! j

goal (1 subgoal):
 1. \<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
unfolding visited_states.simps product_simps
[PROOF STATE]
proof (prove)
using this:
(FSM.initial B # map t_target (right_path p)) ! i = (FSM.initial B # map t_target (right_path p)) ! j

goal (1 subgoal):
 1. \<not> distinct (FSM.initial B # map t_target (right_path p))
[PROOF STEP]
using non_distinct_repetition_indices_rev[OF \<open>i < j\<close> **]
[PROOF STATE]
proof (prove)
using this:
(FSM.initial B # map t_target (right_path p)) ! i = (FSM.initial B # map t_target (right_path p)) ! j
(FSM.initial B # map t_target (right_path p)) ! i = (FSM.initial B # map t_target (right_path p)) ! j \<Longrightarrow> \<not> distinct (FSM.initial B # map t_target (right_path p))

goal (1 subgoal):
 1. \<not> distinct (FSM.initial B # map t_target (right_path p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> distinct (visited_states (FSM.initial B) (right_path p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> distinct (visited_states (FSM.initial B) (right_path p))

goal (1 subgoal):
 1. \<not> FSM.acyclic (Product_FSM.product A B) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
path B (FSM.initial B) (right_path p)
\<not> distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (right_path p)
\<not> distinct (visited_states (FSM.initial B) (right_path p))

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>acyclic B\<close>
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (right_path p)
\<not> distinct (visited_states (FSM.initial B) (right_path p))
FSM.acyclic B

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding acyclic.simps
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (right_path p)
\<not> distinct (visited_states (FSM.initial B) (right_path p))
\<forall>p. path B (FSM.initial B) p \<longrightarrow> distinct (visited_states (FSM.initial B) p)

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
FSM.acyclic (Product_FSM.product A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_product_path_length :
  assumes "acyclic B"
  and     "path (product A B) (initial (product A B)) p"
shows "length p < size B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p < FSM.size B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length p < FSM.size B
[PROOF STEP]
have *:"path B (initial B) (right_path p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path B (FSM.initial B) (right_path p)
[PROOF STEP]
using product_path[of A B] \<open>path (product A B) (initial (product A B)) p\<close>
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (?q1.0, ?q2.0) ?p = (path A ?q1.0 (left_path ?p) \<and> path B ?q2.0 (right_path ?p))
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p

goal (1 subgoal):
 1. path B (FSM.initial B) (right_path p)
[PROOF STEP]
unfolding product_simps
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product A B) (?q1.0, ?q2.0) ?p = (path A ?q1.0 (left_path ?p) \<and> path B ?q2.0 (right_path ?p))
path (Product_FSM.product A B) (FSM.initial A, FSM.initial B) p

goal (1 subgoal):
 1. path B (FSM.initial B) (right_path p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path B (FSM.initial B) (right_path p)

goal (1 subgoal):
 1. length p < FSM.size B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path B (FSM.initial B) (right_path p)
[PROOF STEP]
have **: "distinct (visited_states (initial B) (right_path p))"
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (right_path p)

goal (1 subgoal):
 1. distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (right_path p)
FSM.acyclic B
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p

goal (1 subgoal):
 1. distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
unfolding acyclic.simps
[PROOF STATE]
proof (prove)
using this:
path B (FSM.initial B) (right_path p)
\<forall>p. path B (FSM.initial B) p \<longrightarrow> distinct (visited_states (FSM.initial B) p)
path (Product_FSM.product A B) (FSM.initial (Product_FSM.product A B)) p

goal (1 subgoal):
 1. distinct (visited_states (FSM.initial B) (right_path p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct (visited_states (FSM.initial B) (right_path p))

goal (1 subgoal):
 1. length p < FSM.size B
[PROOF STEP]
have "length (right_path p) < size B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (right_path p) < FSM.size B
[PROOF STEP]
using acyclic_path_length_limit[OF * **]
[PROOF STATE]
proof (prove)
using this:
length (right_path p) < FSM.size B

goal (1 subgoal):
 1. length (right_path p) < FSM.size B
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
length (right_path p) < FSM.size B

goal (1 subgoal):
 1. length p < FSM.size B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (right_path p) < FSM.size B
[PROOF STEP]
show "length p < size B"
[PROOF STATE]
proof (prove)
using this:
length (right_path p) < FSM.size B

goal (1 subgoal):
 1. length p < FSM.size B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length p < FSM.size B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_language_alt_def :
  assumes "acyclic A"
  shows "image p_io (acyclic_paths_up_to_length A (initial A) (size A - 1)) = L A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = L A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = L A
[PROOF STEP]
let ?ps = "acyclic_paths_up_to_length A (initial A) (size A - 1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = L A
[PROOF STEP]
have "\<And> p . path A (initial A) p \<Longrightarrow> length p \<le> FSM.size A - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. path A (FSM.initial A) p \<Longrightarrow> length p \<le> FSM.size A - 1
[PROOF STEP]
using acyclic_path_length_limit assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>path ?M ?q ?p; distinct (visited_states ?q ?p)\<rbrakk> \<Longrightarrow> length ?p < FSM.size ?M
FSM.acyclic A

goal (1 subgoal):
 1. \<And>p. path A (FSM.initial A) p \<Longrightarrow> length p \<le> FSM.size A - 1
[PROOF STEP]
unfolding acyclic.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>path ?M ?q ?p; distinct (visited_states ?q ?p)\<rbrakk> \<Longrightarrow> length ?p < FSM.size ?M
\<forall>p. path A (FSM.initial A) p \<longrightarrow> distinct (visited_states (FSM.initial A) p)

goal (1 subgoal):
 1. \<And>p. path A (FSM.initial A) p \<Longrightarrow> length p \<le> FSM.size A - 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
path A (FSM.initial A) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1

goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = L A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path A (FSM.initial A) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1
[PROOF STEP]
have "?ps = {p. path A (initial A) p}"
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1

goal (1 subgoal):
 1. acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = {p. path A (FSM.initial A) p}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1
FSM.acyclic A

goal (1 subgoal):
 1. acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = {p. path A (FSM.initial A) p}
[PROOF STEP]
unfolding acyclic_paths_up_to_length.simps acyclic.simps
[PROOF STATE]
proof (prove)
using this:
path A (FSM.initial A) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1
\<forall>p. path A (FSM.initial A) p \<longrightarrow> distinct (visited_states (FSM.initial A) p)

goal (1 subgoal):
 1. {p. path A (FSM.initial A) p \<and> length p \<le> FSM.size A - 1 \<and> distinct (visited_states (FSM.initial A) p)} = {p. path A (FSM.initial A) p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = {p. path A (FSM.initial A) p}

goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = L A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = {p. path A (FSM.initial A) p}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = {p. path A (FSM.initial A) p}

goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = L A
[PROOF STEP]
unfolding LS.simps
[PROOF STATE]
proof (prove)
using this:
acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = {p. path A (FSM.initial A) p}

goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = {p_io p |p. path A (FSM.initial A) p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p_io ` acyclic_paths_up_to_length A (FSM.initial A) (FSM.size A - 1) = L A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acyclic_language_intersection_completeness :
  assumes "acyclic A"
  shows "acyclic_language_intersection M A = L M \<inter> L A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
let ?P = "product M A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
let ?ps = "acyclic_paths_up_to_length ?P (initial ?P) (size A - 1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
have "L ?P = L M \<inter> L A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L (Product_FSM.product M A) = L M \<inter> L A
[PROOF STEP]
using product_language
[PROOF STATE]
proof (prove)
using this:
L (Product_FSM.product ?A ?B) = L ?A \<inter> L ?B

goal (1 subgoal):
 1. L (Product_FSM.product M A) = L M \<inter> L A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
L (Product_FSM.product M A) = L M \<inter> L A

goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
have "\<And> p . path ?P (initial ?P) p \<Longrightarrow> length p \<le> FSM.size A - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p \<Longrightarrow> length p \<le> FSM.size A - 1
[PROOF STEP]
using acyclic_product_path_length[OF assms]
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product ?A A) (FSM.initial (Product_FSM.product ?A A)) ?p \<Longrightarrow> length ?p < FSM.size A

goal (1 subgoal):
 1. \<And>p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p \<Longrightarrow> length p \<le> FSM.size A - 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1

goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1
[PROOF STEP]
have "?ps = {p. path ?P (initial ?P) p}"
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1

goal (1 subgoal):
 1. acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = {p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p}
[PROOF STEP]
using acyclic_product[OF assms]
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1
FSM.acyclic (Product_FSM.product ?A A)

goal (1 subgoal):
 1. acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = {p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p}
[PROOF STEP]
unfolding acyclic_paths_up_to_length.simps acyclic.simps
[PROOF STATE]
proof (prove)
using this:
path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) ?p \<Longrightarrow> length ?p \<le> FSM.size A - 1
\<forall>p. path (Product_FSM.product ?A A) (FSM.initial (Product_FSM.product ?A A)) p \<longrightarrow> distinct (visited_states (FSM.initial (Product_FSM.product ?A A)) p)

goal (1 subgoal):
 1. {p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p \<and> length p \<le> FSM.size A - 1 \<and> distinct (visited_states (FSM.initial (Product_FSM.product M A)) p)} = {p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = {p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p}

goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = {p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p}
[PROOF STEP]
have "image p_io ?ps = L ?P"
[PROOF STATE]
proof (prove)
using this:
acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = {p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p}

goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = L (Product_FSM.product M A)
[PROOF STEP]
unfolding LS.simps
[PROOF STATE]
proof (prove)
using this:
acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = {p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p}

goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = {p_io p |p. path (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) p}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p_io ` acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = L (Product_FSM.product M A)

goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p_io ` acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = L (Product_FSM.product M A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p_io ` acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = L (Product_FSM.product M A)

goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
using product_language
[PROOF STATE]
proof (prove)
using this:
p_io ` acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = L (Product_FSM.product M A)
L (Product_FSM.product ?A ?B) = L ?A \<inter> L ?B

goal (1 subgoal):
 1. acyclic_language_intersection M A = L M \<inter> L A
[PROOF STEP]
unfolding acyclic_language_intersection_def Let_def
[PROOF STATE]
proof (prove)
using this:
p_io ` acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = L (Product_FSM.product M A)
L (Product_FSM.product ?A ?B) = L ?A \<inter> L ?B

goal (1 subgoal):
 1. p_io ` acyclic_paths_up_to_length (Product_FSM.product M A) (FSM.initial (Product_FSM.product M A)) (FSM.size A - 1) = L M \<inter> L A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
acyclic_language_intersection M A = L M \<inter> L A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_partition_on_insert_with_fixed_card_eq:
  assumes "finite A"
  assumes "a \<notin> A"
  shows "{P. partition_on (insert a A) P \<and> card P = Suc k} = (do {
     P <- {P. partition_on A P \<and> card P = Suc k};
     p <- P;
     {insert (insert a p) (P - {p})}
  })
  \<union> (do {
    P <- {P. partition_on A P \<and> card P = k};
    {insert {a} P}
  })" (is "?S = ?T")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {P. partition_on (insert a A) P \<and> card P = Suc k} = ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {P. partition_on (insert a A) P \<and> card P = Suc k} \<subseteq> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})) \<subseteq> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
show "?S \<subseteq> ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {P. partition_on (insert a A) P \<and> card P = Suc k} \<subseteq> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (insert a A) P \<and> card P = Suc k} \<Longrightarrow> x \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (insert a A) P \<and> card P = Suc k} \<Longrightarrow> x \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
assume "P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}"
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (insert a A) P \<and> card P = Suc k} \<Longrightarrow> x \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
have "partition_on (insert a A) P" and "card P = Suc k"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}

goal (1 subgoal):
 1. partition_on (insert a A) P &&& card P = Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partition_on (insert a A) P
card P = Suc k

goal (1 subgoal):
 1. \<And>x. x \<in> {P. partition_on (insert a A) P \<and> card P = Suc k} \<Longrightarrow> x \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
show "P \<in> ?T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. \<not> ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
assume "{a} \<in> P"
[PROOF STATE]
proof (state)
this:
{a} \<in> P

goal (2 subgoals):
 1. ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. \<not> ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
have "partition_on A (P - {{a}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on A (P - {{a}})
[PROOF STEP]
using \<open>{a} \<in> P\<close> \<open>partition_on (insert a A) P\<close>[THEN partition_on_Diff, of "{{a}}"] \<open>a \<notin> A\<close>
[PROOF STATE]
proof (prove)
using this:
{a} \<in> P
{{a}} \<subseteq> P \<Longrightarrow> partition_on (insert a A - \<Union> {{a}}) (P - {{a}})
a \<notin> A

goal (1 subgoal):
 1. partition_on A (P - {{a}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
partition_on A (P - {{a}})

goal (2 subgoals):
 1. ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. \<not> ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partition_on A (P - {{a}})

goal (2 subgoals):
 1. ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. \<not> ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from \<open>{a} \<in> P\<close> \<open>card P = Suc k\<close>
[PROOF STATE]
proof (chain)
picking this:
{a} \<in> P
card P = Suc k
[PROOF STEP]
have "card (P - {{a}}) = k"
[PROOF STATE]
proof (prove)
using this:
{a} \<in> P
card P = Suc k

goal (1 subgoal):
 1. card (P - {{a}}) = k
[PROOF STEP]
by (subst card_Diff_singleton) (auto intro: card_ge_0_finite)
[PROOF STATE]
proof (state)
this:
card (P - {{a}}) = k

goal (2 subgoals):
 1. ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. \<not> ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (P - {{a}}) = k

goal (2 subgoals):
 1. ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. \<not> ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from \<open>{a} \<in> P\<close>
[PROOF STATE]
proof (chain)
picking this:
{a} \<in> P
[PROOF STEP]
have "P = insert {a} (P - {{a}})"
[PROOF STATE]
proof (prove)
using this:
{a} \<in> P

goal (1 subgoal):
 1. P = insert {a} (P - {{a}})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P = insert {a} (P - {{a}})

goal (2 subgoals):
 1. ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. \<not> ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partition_on A (P - {{a}})
card (P - {{a}}) = k
P = insert {a} (P - {{a}})
[PROOF STEP]
have "P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})"
[PROOF STATE]
proof (prove)
using this:
partition_on A (P - {{a}})
card (P - {{a}}) = k
P = insert {a} (P - {{a}})

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})

goal (2 subgoals):
 1. ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
 2. \<not> ?P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})

goal (1 subgoal):
 1. P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
assume "{a} \<notin> P"
[PROOF STATE]
proof (state)
this:
{a} \<notin> P

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
let ?p' = "(THE X. a \<in> X \<and> X \<in> P)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
let ?p = "(THE X. a \<in> X \<and> X \<in> P) - {a}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
let ?P' = "insert ?p (P - {?p'})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
[PROOF STEP]
have "a \<in> (THE X. a \<in> X \<and> X \<in> P)"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P

goal (1 subgoal):
 1. a \<in> (THE X. a \<in> X \<and> X \<in> P)
[PROOF STEP]
using partition_on_in_the_unique_part
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
\<lbrakk>partition_on ?A ?P; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<in> (THE X. ?x \<in> X \<and> X \<in> ?P)

goal (1 subgoal):
 1. a \<in> (THE X. a \<in> X \<and> X \<in> P)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a \<in> (THE X. a \<in> X \<and> X \<in> P)

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
[PROOF STEP]
have "(THE X. a \<in> X \<and> X \<in> P) \<in> P"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P

goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
using partition_on_the_part_mem
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
\<lbrakk>partition_on ?A ?P; ?x \<in> ?A\<rbrakk> \<Longrightarrow> (THE X. ?x \<in> X \<and> X \<in> ?P) \<in> ?P

goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) \<in> P
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(THE X. a \<in> X \<and> X \<in> P) \<in> P

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from this \<open>partition_on (insert a A) P\<close>
[PROOF STATE]
proof (chain)
picking this:
(THE X. a \<in> X \<and> X \<in> P) \<in> P
partition_on (insert a A) P
[PROOF STEP]
have "(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P"
[PROOF STATE]
proof (prove)
using this:
(THE X. a \<in> X \<and> X \<in> P) \<in> P
partition_on (insert a A) P

goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P
[PROOF STEP]
using partition_subset_imp_notin \<open>a \<in> (THE X. a \<in> X \<and> X \<in> P)\<close>
[PROOF STATE]
proof (prove)
using this:
(THE X. a \<in> X \<and> X \<in> P) \<in> P
partition_on (insert a A) P
\<lbrakk>partition_on ?A ?P; ?X \<in> ?P; ?X' \<subset> ?X\<rbrakk> \<Longrightarrow> ?X' \<notin> ?P
a \<in> (THE X. a \<in> X \<and> X \<in> P)

goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
have "(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}
[PROOF STEP]
using \<open>(THE X. a \<in> X \<and> X \<in> P) \<in> P\<close> \<open>{a} \<notin> P\<close>
[PROOF STATE]
proof (prove)
using this:
(THE X. a \<in> X \<and> X \<in> P) \<in> P
{a} \<notin> P

goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
[PROOF STEP]
have "(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P

goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A
[PROOF STEP]
using \<open>(THE X. a \<in> X \<and> X \<in> P) \<in> P\<close> partition_onD1
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
(THE X. a \<in> X \<and> X \<in> P) \<in> P
partition_on ?A ?P \<Longrightarrow> ?A = \<Union> ?P

goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
note facts_on_the_part_of = \<open>a \<in> (THE X. a \<in> X \<and> X \<in> P)\<close> \<open>(THE X. a \<in> X \<and> X \<in> P) \<in> P\<close>
        \<open>(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P\<close> \<open>(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}\<close>
        \<open>(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A\<close>
[PROOF STATE]
proof (state)
this:
a \<in> (THE X. a \<in> X \<and> X \<in> P)
(THE X. a \<in> X \<and> X \<in> P) \<in> P
(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P
(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}
(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close> \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
finite A
[PROOF STEP]
have "finite P"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
finite A

goal (1 subgoal):
 1. finite P
[PROOF STEP]
by (meson finite.insertI finite_elements)
[PROOF STATE]
proof (state)
this:
finite P

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from \<open>partition_on (insert a A) P\<close> \<open>a \<notin> A\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on (insert a A) P
a \<notin> A
[PROOF STEP]
have "partition_on (A - ?p) (P - {?p'})"
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
a \<notin> A

goal (1 subgoal):
 1. partition_on (A - ((THE X. a \<in> X \<and> X \<in> P) - {a})) (P - {THE X. a \<in> X \<and> X \<in> P})
[PROOF STEP]
using facts_on_the_part_of
[PROOF STATE]
proof (prove)
using this:
partition_on (insert a A) P
a \<notin> A
a \<in> (THE X. a \<in> X \<and> X \<in> P)
(THE X. a \<in> X \<and> X \<in> P) \<in> P
(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P
(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}
(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A

goal (1 subgoal):
 1. partition_on (A - ((THE X. a \<in> X \<and> X \<in> P) - {a})) (P - {THE X. a \<in> X \<and> X \<in> P})
[PROOF STEP]
by (auto intro: partition_on_remove_singleton)
[PROOF STATE]
proof (state)
this:
partition_on (A - ((THE X. a \<in> X \<and> X \<in> P) - {a})) (P - {THE X. a \<in> X \<and> X \<in> P})

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
partition_on (A - ((THE X. a \<in> X \<and> X \<in> P) - {a})) (P - {THE X. a \<in> X \<and> X \<in> P})
[PROOF STEP]
have "partition_on A ?P'"
[PROOF STATE]
proof (prove)
using this:
partition_on (A - ((THE X. a \<in> X \<and> X \<in> P) - {a})) (P - {THE X. a \<in> X \<and> X \<in> P})

goal (1 subgoal):
 1. partition_on A (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}))
[PROOF STEP]
using facts_on_the_part_of
[PROOF STATE]
proof (prove)
using this:
partition_on (A - ((THE X. a \<in> X \<and> X \<in> P) - {a})) (P - {THE X. a \<in> X \<and> X \<in> P})
a \<in> (THE X. a \<in> X \<and> X \<in> P)
(THE X. a \<in> X \<and> X \<in> P) \<in> P
(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P
(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}
(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A

goal (1 subgoal):
 1. partition_on A (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}))
[PROOF STEP]
by (auto intro: partition_on_insert simp add: disjnt_iff)
[PROOF STATE]
proof (state)
this:
partition_on A (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}))

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partition_on A (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}))

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
have "card ?P' = Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k
[PROOF STEP]
from \<open>card P = Suc k\<close>
[PROOF STATE]
proof (chain)
picking this:
card P = Suc k
[PROOF STEP]
have "card (P - {THE X. a \<in> X \<and> X \<in> P}) = k"
[PROOF STATE]
proof (prove)
using this:
card P = Suc k

goal (1 subgoal):
 1. card (P - {THE X. a \<in> X \<and> X \<in> P}) = k
[PROOF STEP]
using \<open>finite P\<close> \<open>(THE X. a \<in> X \<and> X \<in> P) \<in> P\<close>
[PROOF STATE]
proof (prove)
using this:
card P = Suc k
finite P
(THE X. a \<in> X \<and> X \<in> P) \<in> P

goal (1 subgoal):
 1. card (P - {THE X. a \<in> X \<and> X \<in> P}) = k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (P - {THE X. a \<in> X \<and> X \<in> P}) = k

goal (1 subgoal):
 1. card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
card (P - {THE X. a \<in> X \<and> X \<in> P}) = k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (P - {THE X. a \<in> X \<and> X \<in> P}) = k

goal (1 subgoal):
 1. card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k
[PROOF STEP]
using \<open>finite P\<close> \<open>(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P\<close>
[PROOF STATE]
proof (prove)
using this:
card (P - {THE X. a \<in> X \<and> X \<in> P}) = k
finite P
(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P

goal (1 subgoal):
 1. card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k
[PROOF STEP]
by (simp add: card_insert_if)
[PROOF STATE]
proof (state)
this:
card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
have "?p \<in> ?P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE X. a \<in> X \<and> X \<in> P) - {a} \<in> insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(THE X. a \<in> X \<and> X \<in> P) - {a} \<in> insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(THE X. a \<in> X \<and> X \<in> P) - {a} \<in> insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
have "P = insert (insert a ?p) (?P' - {?p})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = insert (insert a ((THE X. a \<in> X \<and> X \<in> P) - {a})) (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}) - {(THE X. a \<in> X \<and> X \<in> P) - {a}})
[PROOF STEP]
using facts_on_the_part_of
[PROOF STATE]
proof (prove)
using this:
a \<in> (THE X. a \<in> X \<and> X \<in> P)
(THE X. a \<in> X \<and> X \<in> P) \<in> P
(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P
(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}
(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A

goal (1 subgoal):
 1. P = insert (insert a ((THE X. a \<in> X \<and> X \<in> P) - {a})) (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}) - {(THE X. a \<in> X \<and> X \<in> P) - {a}})
[PROOF STEP]
by (auto simp add: insert_absorb)
[PROOF STATE]
proof (state)
this:
P = insert (insert a ((THE X. a \<in> X \<and> X \<in> P) - {a})) (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}) - {(THE X. a \<in> X \<and> X \<in> P) - {a}})

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partition_on A (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}))
card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k
(THE X. a \<in> X \<and> X \<in> P) - {a} \<in> insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})
P = insert (insert a ((THE X. a \<in> X \<and> X \<in> P) - {a})) (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}) - {(THE X. a \<in> X \<and> X \<in> P) - {a}})
[PROOF STEP]
have "P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))"
[PROOF STATE]
proof (prove)
using this:
partition_on A (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}))
card (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})) = Suc k
(THE X. a \<in> X \<and> X \<in> P) - {a} \<in> insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P})
P = insert (insert a ((THE X. a \<in> X \<and> X \<in> P) - {a})) (insert ((THE X. a \<in> X \<and> X \<in> P) - {a}) (P - {THE X. a \<in> X \<and> X \<in> P}) - {(THE X. a \<in> X \<and> X \<in> P) - {a}})

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))

goal (1 subgoal):
 1. {a} \<notin> P \<Longrightarrow> P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))

goal (1 subgoal):
 1. P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{P. partition_on (insert a A) P \<and> card P = Suc k} \<subseteq> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))

goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})) \<subseteq> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})) \<subseteq> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
show "?T \<subseteq> ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})) \<subseteq> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})) \<Longrightarrow> x \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
fix P
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})) \<Longrightarrow> x \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
assume "P \<in> ?T" (is "_ \<in> ?subexpr1 \<union> ?subexpr2")
[PROOF STATE]
proof (state)
this:
P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))

goal (1 subgoal):
 1. \<And>x. x \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})) \<Longrightarrow> x \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))
[PROOF STEP]
show "P \<in> ?S"
[PROOF STATE]
proof (prove)
using this:
P \<in> ({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}))

goal (1 subgoal):
 1. P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
assume "P \<in> ?subexpr1"
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))

goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))
[PROOF STEP]
obtain p P' where "P = insert (insert a p) (P' - {p})"
        and "partition_on A P'" and "card P' = Suc k" and "p \<in> P'"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))

goal (1 subgoal):
 1. (\<And>p P'. \<lbrakk>P = insert (insert a p) (P' - {p}); partition_on A P'; card P' = Suc k; p \<in> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P = insert (insert a p) (P' - {p})
partition_on A P'
card P' = Suc k
p \<in> P'

goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from \<open>p \<in> P'\<close> \<open>partition_on A P'\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<in> P'
partition_on A P'
[PROOF STEP]
have "partition_on (A - p) (P' - {p})"
[PROOF STATE]
proof (prove)
using this:
p \<in> P'
partition_on A P'

goal (1 subgoal):
 1. partition_on (A - p) (P' - {p})
[PROOF STEP]
by (simp add: partition_on_remove_singleton)
[PROOF STATE]
proof (state)
this:
partition_on (A - p) (P' - {p})

goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from \<open>partition_on A P'\<close> \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on A P'
finite A
[PROOF STEP]
have "finite P"
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
finite A

goal (1 subgoal):
 1. finite P
[PROOF STEP]
using \<open>P = _\<close> finite_elements
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
finite A
P = insert (insert a p) (P' - {p})
\<lbrakk>finite ?A; partition_on ?A ?P\<rbrakk> \<Longrightarrow> finite ?P

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

goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from \<open>partition_on A P'\<close> \<open>a \<notin> A\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on A P'
a \<notin> A
[PROOF STEP]
have "insert a p \<notin> P' - {p}"
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
a \<notin> A

goal (1 subgoal):
 1. insert a p \<notin> P' - {p}
[PROOF STEP]
using partition_onD1
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
a \<notin> A
partition_on ?A ?P \<Longrightarrow> ?A = \<Union> ?P

goal (1 subgoal):
 1. insert a p \<notin> P' - {p}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
insert a p \<notin> P' - {p}

goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from \<open>P = _\<close> this \<open>card P' = Suc k\<close> \<open>finite P\<close> \<open>p \<in> P'\<close>
[PROOF STATE]
proof (chain)
picking this:
P = insert (insert a p) (P' - {p})
insert a p \<notin> P' - {p}
card P' = Suc k
finite P
p \<in> P'
[PROOF STEP]
have "card P = Suc k"
[PROOF STATE]
proof (prove)
using this:
P = insert (insert a p) (P' - {p})
insert a p \<notin> P' - {p}
card P' = Suc k
finite P
p \<in> P'

goal (1 subgoal):
 1. card P = Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card P = Suc k

goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card P = Suc k

goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
have "partition_on (insert a A) P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_on (insert a A) P
[PROOF STEP]
using \<open>partition_on (A - p) (P' - {p})\<close> \<open>a \<notin> A\<close> \<open>p \<in> P'\<close> \<open>partition_on A P'\<close> \<open>P = _\<close>
[PROOF STATE]
proof (prove)
using this:
partition_on (A - p) (P' - {p})
a \<notin> A
p \<in> P'
partition_on A P'
P = insert (insert a p) (P' - {p})

goal (1 subgoal):
 1. partition_on (insert a A) P
[PROOF STEP]
by (auto intro!: partition_on_insert dest: partition_onD1 simp add: disjnt_iff)
[PROOF STATE]
proof (state)
this:
partition_on (insert a A) P

goal (2 subgoals):
 1. P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
 2. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card P = Suc k
partition_on (insert a A) P
[PROOF STEP]
show "P \<in> ?S"
[PROOF STATE]
proof (prove)
using this:
card P = Suc k
partition_on (insert a A) P

goal (1 subgoal):
 1. P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
assume "P \<in> ?subexpr2"
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})
[PROOF STEP]
obtain P' where "P = insert {a} P'" and "partition_on A P'" and "card P' = k"
[PROOF STATE]
proof (prove)
using this:
P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P = insert {a} P'; partition_on A P'; card P' = k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P = insert {a} P'
partition_on A P'
card P' = k

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from \<open>partition_on A P'\<close> \<open>finite A\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on A P'
finite A
[PROOF STEP]
have "finite P"
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
finite A

goal (1 subgoal):
 1. finite P
[PROOF STEP]
using \<open>P = insert {a} P'\<close> finite_elements
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
finite A
P = insert {a} P'
\<lbrakk>finite ?A; partition_on ?A ?P\<rbrakk> \<Longrightarrow> finite ?P

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

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from \<open>partition_on A P'\<close> \<open>a \<notin> A\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on A P'
a \<notin> A
[PROOF STEP]
have "{a} \<notin> P'"
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
a \<notin> A

goal (1 subgoal):
 1. {a} \<notin> P'
[PROOF STEP]
using partition_onD1
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
a \<notin> A
partition_on ?A ?P \<Longrightarrow> ?A = \<Union> ?P

goal (1 subgoal):
 1. {a} \<notin> P'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{a} \<notin> P'

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from \<open>P = insert {a} P'\<close> \<open>card P' = k\<close> this \<open>finite P\<close>
[PROOF STATE]
proof (chain)
picking this:
P = insert {a} P'
card P' = k
{a} \<notin> P'
finite P
[PROOF STEP]
have "card P = Suc k"
[PROOF STATE]
proof (prove)
using this:
P = insert {a} P'
card P' = k
{a} \<notin> P'
finite P

goal (1 subgoal):
 1. card P = Suc k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card P = Suc k

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card P = Suc k

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
from \<open>partition_on A P'\<close> \<open>a \<notin> A\<close>
[PROOF STATE]
proof (chain)
picking this:
partition_on A P'
a \<notin> A
[PROOF STEP]
have "partition_on (insert a A) P"
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
a \<notin> A

goal (1 subgoal):
 1. partition_on (insert a A) P
[PROOF STEP]
using \<open>P = insert {a} P'\<close>
[PROOF STATE]
proof (prove)
using this:
partition_on A P'
a \<notin> A
P = insert {a} P'

goal (1 subgoal):
 1. partition_on (insert a A) P
[PROOF STEP]
by (simp add: partition_on_insert_singleton)
[PROOF STATE]
proof (state)
this:
partition_on (insert a A) P

goal (1 subgoal):
 1. P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P}) \<Longrightarrow> P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card P = Suc k
partition_on (insert a A) P
[PROOF STEP]
show "P \<in> ?S"
[PROOF STATE]
proof (prove)
using this:
card P = Suc k
partition_on (insert a A) P

goal (1 subgoal):
 1. P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
({P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))) \<union> ({P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})) \<subseteq> {P. partition_on (insert a A) P \<and> card P = Suc k}

goal:
No subgoals!
[PROOF STEP]
qed