[STATEMENT]
lemma find_graph_occurence:
  assumes "chain S" "finite E" "finite V" "graph_homomorphism (LG E V) (chain_sup S) f"
  shows "\<exists> i. graph_homomorphism (LG E V) (S i) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
have [simp]:"restrict (S i) = S i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict (S i) = S i
[PROOF STEP]
using chain[OF assms(1),unfolded subgraph_def,of i i]
[PROOF STATE]
proof (prove)
using this:
i \<le> i \<Longrightarrow> graph (S i) \<and> graph (S i) \<and> graph_union (S i) (S i) = S i

goal (1 subgoal):
 1. restrict (S i) = S i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
restrict (S ?i) = S ?i

goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
from assms[unfolded graph_homomorphism_def edge_preserving labeled_graph.sel]
[PROOF STATE]
proof (chain)
picking this:
chain S
finite E
finite V
V = Domain f \<and> graph (LG E V) \<and> graph (chain_sup S) \<and> f `` V \<subseteq> vertices (chain_sup S) \<and> univalent f \<and> on_triple f `` E \<subseteq> edges (chain_sup S)
[PROOF STEP]
have u:"univalent f"
   and e:"on_triple f `` E \<subseteq> edges (chain_sup S)"
   and v:"f `` V \<subseteq> vertices (chain_sup S)"
[PROOF STATE]
proof (prove)
using this:
chain S
finite E
finite V
V = Domain f \<and> graph (LG E V) \<and> graph (chain_sup S) \<and> f `` V \<subseteq> vertices (chain_sup S) \<and> univalent f \<and> on_triple f `` E \<subseteq> edges (chain_sup S)

goal (1 subgoal):
 1. univalent f &&& on_triple f `` E \<subseteq> edges (chain_sup S) &&& f `` V \<subseteq> vertices (chain_sup S)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
univalent f
on_triple f `` E \<subseteq> edges (chain_sup S)
f `` V \<subseteq> vertices (chain_sup S)

goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
from find_graph_occurence_edges[OF assms(1,2) u e]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. on_triple f `` E \<subseteq> edges (S i)
[PROOF STEP]
obtain i where i:"on_triple f `` E \<subseteq> edges (S i)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. on_triple f `` E \<subseteq> edges (S i)

goal (1 subgoal):
 1. (\<And>i. on_triple f `` E \<subseteq> edges (S i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
on_triple f `` E \<subseteq> edges (S i)

goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
from find_graph_occurence_vertices[OF assms(1,3) u v]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. f `` V \<subseteq> vertices (S i)
[PROOF STEP]
obtain j where j:"f `` V \<subseteq> vertices (S j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. f `` V \<subseteq> vertices (S i)

goal (1 subgoal):
 1. (\<And>j. f `` V \<subseteq> vertices (S j) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f `` V \<subseteq> vertices (S j)

goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
have sg:"subgraph (S i) (S (max i j))" "subgraph (S j) (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (S i) (S (max i j)) &&& subgraph (S j) (S (max i j))
[PROOF STEP]
by(rule chain[OF assms(1)],force)+
[PROOF STATE]
proof (state)
this:
subgraph (S i) (S (max i j))
subgraph (S j) (S (max i j))

goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
have e:"on_triple f `` E \<subseteq> edges (S (max i j))"
   and v:"f `` V \<subseteq> vertices (S (max i j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. on_triple f `` E \<subseteq> edges (S (max i j)) &&& f `` V \<subseteq> vertices (S (max i j))
[PROOF STEP]
using i j subgraph_subset(2)[OF sg(1)] subgraph_subset(1)[OF sg(2)]
[PROOF STATE]
proof (prove)
using this:
on_triple f `` E \<subseteq> edges (S i)
f `` V \<subseteq> vertices (S j)
edges (restrict (S i)) \<subseteq> edges (S (max i j))
vertices (S j) \<subseteq> vertices (S (max i j))

goal (1 subgoal):
 1. on_triple f `` E \<subseteq> edges (S (max i j)) &&& f `` V \<subseteq> vertices (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
on_triple f `` E \<subseteq> edges (S (max i j))
f `` V \<subseteq> vertices (S (max i j))

goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
have "graph_homomorphism (LG E V) (S (max i j)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_homomorphism (LG E V) (S (max i j)) f
[PROOF STEP]
proof(rule graph_homomorphismI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. vertices (LG E V) = Domain f
 2. f `` vertices (LG E V) \<subseteq> vertices (S (max i j))
 3. univalent f
 4. edge_preserving f (edges (LG E V)) (edges (S (max i j)))
 5. graph (LG E V)
 6. graph (S (max i j))
[PROOF STEP]
from assms[unfolded graph_homomorphism_def edge_preserving labeled_graph.sel] e v
[PROOF STATE]
proof (chain)
picking this:
chain S
finite E
finite V
V = Domain f \<and> graph (LG E V) \<and> graph (chain_sup S) \<and> f `` V \<subseteq> vertices (chain_sup S) \<and> univalent f \<and> on_triple f `` E \<subseteq> edges (chain_sup S)
on_triple f `` E \<subseteq> edges (S (max i j))
f `` V \<subseteq> vertices (S (max i j))
[PROOF STEP]
show "vertices (LG E V) = Domain f"
     and "univalent f"
     and "LG E V = restrict (LG E V)"
     and "f `` vertices (LG E V) \<subseteq> vertices (S (max i j))"
     and "edge_preserving f (edges (LG E V)) (edges (S (max i j)))"
     and "S (max i j) = restrict (S (max i j))"
[PROOF STATE]
proof (prove)
using this:
chain S
finite E
finite V
V = Domain f \<and> graph (LG E V) \<and> graph (chain_sup S) \<and> f `` V \<subseteq> vertices (chain_sup S) \<and> univalent f \<and> on_triple f `` E \<subseteq> edges (chain_sup S)
on_triple f `` E \<subseteq> edges (S (max i j))
f `` V \<subseteq> vertices (S (max i j))

goal (1 subgoal):
 1. (vertices (LG E V) = Domain f &&& univalent f &&& graph (LG E V)) &&& f `` vertices (LG E V) \<subseteq> vertices (S (max i j)) &&& edge_preserving f (edges (LG E V)) (edges (S (max i j))) &&& graph (S (max i j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vertices (LG E V) = Domain f
univalent f
graph (LG E V)
f `` vertices (LG E V) \<subseteq> vertices (S (max i j))
edge_preserving f (edges (LG E V)) (edges (S (max i j)))
graph (S (max i j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG E V) (S (max i j)) f

goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG E V) (S (max i j)) f

goal (1 subgoal):
 1. \<exists>i. graph_homomorphism (LG E V) (S i) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. graph_homomorphism (LG E V) (S i) f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fair_chain_impl_consequence_graph:
  assumes "fair_chain Rs S" "\<And> R. R \<in> Rs \<Longrightarrow> subgraph (fst R) (snd R) \<and> finite_graph (fst R)"
  shows "consequence_graph Rs (chain_sup S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
fix R
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
assume a:"R \<in> Rs"
[PROOF STATE]
proof (state)
this:
R \<in> Rs

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
have fin_v:"finite (vertices (fst R))" and fin_e: "finite (edges (fst R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vertices (fst R)) &&& finite (edges (fst R))
[PROOF STEP]
using assms(2)[OF a]
[PROOF STATE]
proof (prove)
using this:
subgraph (fst R) (snd R) \<and> finite_graph (fst R)

goal (1 subgoal):
 1. finite (vertices (fst R)) &&& finite (edges (fst R))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (vertices (fst R))
finite (edges (fst R))

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite (vertices (fst R))
finite (edges (fst R))

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
assume "graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) f"
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) f

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
with find_graph_occurence[OF fair_chainD(1)[OF assms(1)] fin_e fin_v]
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) ?f \<Longrightarrow> \<exists>i. graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (S i) ?f
graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) f
[PROOF STEP]
obtain i where "graph_homomorphism (fst R) (S i) f"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) ?f \<Longrightarrow> \<exists>i. graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (S i) ?f
graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) f

goal (1 subgoal):
 1. (\<And>i. graph_homomorphism (fst R) (S i) f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (fst R) (S i) f

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
from fair_chainD(2)[OF assms(1) a this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>j. extensible R (S j) f
[PROOF STEP]
obtain j
         where "extensible R (S j) f"
[PROOF STATE]
proof (prove)
using this:
\<exists>j. extensible R (S j) f

goal (1 subgoal):
 1. (\<And>j. extensible R (S j) f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
extensible R (S j) f

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
hence "extensible R (chain_sup S) f"
[PROOF STATE]
proof (prove)
using this:
extensible R (S j) f

goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
using fair_chainD(1)[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
extensible R (S j) f
chain S

goal (1 subgoal):
 1. extensible R (chain_sup S) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extensible R (chain_sup S) f

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) ?f2 \<Longrightarrow> extensible R (chain_sup S) ?f2

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
hence "maintained R (chain_sup S)"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) ?f2 \<Longrightarrow> extensible R (chain_sup S) ?f2

goal (1 subgoal):
 1. maintained R (chain_sup S)
[PROOF STEP]
unfolding maintained_def
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (LG (edges (fst R)) (vertices (fst R))) (chain_sup S) ?f2 \<Longrightarrow> extensible R (chain_sup S) ?f2

goal (1 subgoal):
 1. \<forall>f. graph_homomorphism (fst R) (chain_sup S) f \<longrightarrow> extensible R (chain_sup S) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
maintained R (chain_sup S)

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?R2 \<in> Rs \<Longrightarrow> maintained ?R2 (chain_sup S)

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
note mnt = this
[PROOF STATE]
proof (state)
this:
?R2 \<in> Rs \<Longrightarrow> maintained ?R2 (chain_sup S)

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
fair_chain Rs S
?R \<in> Rs \<Longrightarrow> subgraph (fst ?R) (snd ?R) \<and> finite_graph (fst ?R)
[PROOF STEP]
have "chain S"
[PROOF STATE]
proof (prove)
using this:
fair_chain Rs S
?R \<in> Rs \<Longrightarrow> subgraph (fst ?R) (snd ?R) \<and> finite_graph (fst ?R)

goal (1 subgoal):
 1. chain S
[PROOF STEP]
unfolding fair_chain_def
[PROOF STATE]
proof (prove)
using this:
chain S \<and> (\<forall>R f i. R \<in> Rs \<and> graph_homomorphism (fst R) (S i) f \<longrightarrow> (\<exists>j. extensible R (S j) f))
?R \<in> Rs \<Longrightarrow> subgraph (fst ?R) (snd ?R) \<and> finite_graph (fst ?R)

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

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
chain S

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S)
[PROOF STEP]
unfolding consequence_graph_def
[PROOF STATE]
proof (prove)
using this:
chain S

goal (1 subgoal):
 1. graph (chain_sup S) \<and> (\<forall>R\<in>Rs. subgraph (fst R) (snd R) \<and> maintained R (chain_sup S))
[PROOF STEP]
using mnt assms(2)
[PROOF STATE]
proof (prove)
using this:
chain S
?R2 \<in> Rs \<Longrightarrow> maintained ?R2 (chain_sup S)
?R \<in> Rs \<Longrightarrow> subgraph (fst ?R) (snd ?R) \<and> finite_graph (fst ?R)

goal (1 subgoal):
 1. graph (chain_sup S) \<and> (\<forall>R\<in>Rs. subgraph (fst R) (snd R) \<and> maintained R (chain_sup S))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
consequence_graph Rs (chain_sup S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weak_universalD[dest]:
  assumes "weak_universal (t:: 'x itself) R (G\<^sub>1::('a, 'b) labeled_graph) G\<^sub>2 f\<^sub>1 f\<^sub>2"
  shows "\<And>  h\<^sub>1 h\<^sub>2 G::('a, 'x) labeled_graph.
         graph_homomorphism (snd R) G h\<^sub>1 \<Longrightarrow> graph_homomorphism G\<^sub>1 G h\<^sub>2 \<Longrightarrow> f\<^sub>1 O h\<^sub>2 \<subseteq> h\<^sub>1
         \<Longrightarrow> (\<exists> h. graph_homomorphism G\<^sub>2 G h \<and> h\<^sub>2 \<subseteq> h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h\<^sub>1 h\<^sub>2 G. \<lbrakk>graph_homomorphism (snd R) G h\<^sub>1; graph_homomorphism G\<^sub>1 G h\<^sub>2; f\<^sub>1 O h\<^sub>2 \<subseteq> h\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism G\<^sub>2 G h \<and> h\<^sub>2 \<subseteq> h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
weak_universal t R G\<^sub>1 G\<^sub>2 f\<^sub>1 f\<^sub>2

goal (1 subgoal):
 1. \<And>h\<^sub>1 h\<^sub>2 G. \<lbrakk>graph_homomorphism (snd R) G h\<^sub>1; graph_homomorphism G\<^sub>1 G h\<^sub>2; f\<^sub>1 O h\<^sub>2 \<subseteq> h\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism G\<^sub>2 G h \<and> h\<^sub>2 \<subseteq> h
[PROOF STEP]
unfolding weak_universal_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h\<^sub>1 h\<^sub>2 G. graph_homomorphism (snd R) G h\<^sub>1 \<and> graph_homomorphism G\<^sub>1 G h\<^sub>2 \<and> f\<^sub>1 O h\<^sub>2 \<subseteq> h\<^sub>1 \<longrightarrow> (\<exists>h. graph_homomorphism G\<^sub>2 G h \<and> h\<^sub>2 \<subseteq> h)

goal (1 subgoal):
 1. \<And>h\<^sub>1 h\<^sub>2 G. \<lbrakk>graph_homomorphism (snd R) G h\<^sub>1; graph_homomorphism G\<^sub>1 G h\<^sub>2; f\<^sub>1 O h\<^sub>2 \<subseteq> h\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism G\<^sub>2 G h \<and> h\<^sub>2 \<subseteq> h
[PROOF STEP]
by metis


[STATEMENT]
lemma weak_universalI[intro]:
  assumes "\<And> h\<^sub>1 h\<^sub>2 G::('a, 'x) labeled_graph.
         graph_homomorphism (snd R) G h\<^sub>1 \<Longrightarrow> graph_homomorphism G\<^sub>1 G h\<^sub>2 \<Longrightarrow> f\<^sub>1 O h\<^sub>2 \<subseteq> h\<^sub>1
         \<Longrightarrow> (\<exists> h. graph_homomorphism G\<^sub>2 G h \<and> h\<^sub>2 \<subseteq> h)"
  shows "weak_universal (t:: 'x itself) R (G\<^sub>1::('a, 'b) labeled_graph) G\<^sub>2 f\<^sub>1 f\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_universal t R G\<^sub>1 G\<^sub>2 f\<^sub>1 f\<^sub>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>graph_homomorphism (snd R) ?G ?h\<^sub>1; graph_homomorphism G\<^sub>1 ?G ?h\<^sub>2; f\<^sub>1 O ?h\<^sub>2 \<subseteq> ?h\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism G\<^sub>2 ?G h \<and> ?h\<^sub>2 \<subseteq> h

goal (1 subgoal):
 1. weak_universal t R G\<^sub>1 G\<^sub>2 f\<^sub>1 f\<^sub>2
[PROOF STEP]
unfolding weak_universal_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>graph_homomorphism (snd R) ?G ?h\<^sub>1; graph_homomorphism G\<^sub>1 ?G ?h\<^sub>2; f\<^sub>1 O ?h\<^sub>2 \<subseteq> ?h\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism G\<^sub>2 ?G h \<and> ?h\<^sub>2 \<subseteq> h

goal (1 subgoal):
 1. \<forall>h\<^sub>1 h\<^sub>2 G. graph_homomorphism (snd R) G h\<^sub>1 \<and> graph_homomorphism G\<^sub>1 G h\<^sub>2 \<and> f\<^sub>1 O h\<^sub>2 \<subseteq> h\<^sub>1 \<longrightarrow> (\<exists>h. graph_homomorphism G\<^sub>2 G h \<and> h\<^sub>2 \<subseteq> h)
[PROOF STEP]
by force


[STATEMENT]
lemma Simple_WPCI [intro]:
  assumes "set_of_graph_rules Rs" "graph (S 0)"
          "\<And> i. (S i = S (Suc i)) \<or> (\<exists> R \<in> Rs. pushout_step t R (S i) (S (Suc i)))"
        shows "Simple_WPC t Rs S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Simple_WPC t Rs S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Simple_WPC t Rs S
[PROOF STEP]
have "graph (S i)" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph (S i)
[PROOF STEP]
proof(induct i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. graph (S 0)
 2. \<And>i. graph (S i) \<Longrightarrow> graph (S (Suc i))
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
graph (S i)

goal (2 subgoals):
 1. graph (S 0)
 2. \<And>i. graph (S i) \<Longrightarrow> graph (S (Suc i))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
graph (S i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
graph (S i)

goal (1 subgoal):
 1. graph (S (Suc i))
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
graph (S i)
S ?i = S (Suc ?i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S ?i) (S (Suc ?i)))

goal (1 subgoal):
 1. graph (S (Suc i))
[PROOF STEP]
unfolding pushout_step_def subgraph_def
[PROOF STATE]
proof (prove)
using this:
graph (S i)
S ?i = S (Suc ?i) \<or> (\<exists>R\<in>Rs. (graph (S ?i) \<and> graph (S (Suc ?i)) \<and> graph_union (S ?i) (S (Suc ?i)) = S (Suc ?i)) \<and> (\<exists>f\<^sub>1 f\<^sub>2. graph_homomorphism (fst R) (S ?i) f\<^sub>1 \<and> graph_homomorphism (snd R) (S (Suc ?i)) f\<^sub>2 \<and> f\<^sub>1 \<subseteq> f\<^sub>2 \<and> weak_universal t R (S ?i) (S (Suc ?i)) f\<^sub>1 f\<^sub>2))

goal (1 subgoal):
 1. graph (S (Suc i))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
graph (S (Suc i))

goal (1 subgoal):
 1. graph (S 0)
[PROOF STEP]
qed (fact assms)
[PROOF STATE]
proof (state)
this:
graph (S ?i)

goal (1 subgoal):
 1. Simple_WPC t Rs S
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
graph (S ?i)

goal (1 subgoal):
 1. Simple_WPC t Rs S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
graph (S ?i)
set_of_graph_rules Rs
graph (S 0)
S ?i = S (Suc ?i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S ?i) (S (Suc ?i)))

goal (1 subgoal):
 1. Simple_WPC t Rs S
[PROOF STEP]
unfolding Simple_WPC_def
[PROOF STATE]
proof (prove)
using this:
graph (S ?i)
set_of_graph_rules Rs
graph (S 0)
S ?i = S (Suc ?i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S ?i) (S (Suc ?i)))

goal (1 subgoal):
 1. set_of_graph_rules Rs \<and> (\<forall>i. graph (S i) \<and> S i = S (Suc i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S i) (S (Suc i))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Simple_WPC t Rs S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Simple_WPC_Chain[simp]:
  assumes "Simple_WPC t Rs S"
  shows "chain S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. chain S
[PROOF STEP]
have "subgraph (S i) (S (Suc i))" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgraph (S i) (S (Suc i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Simple_WPC t Rs S

goal (1 subgoal):
 1. subgraph (S i) (S (Suc i))
[PROOF STEP]
unfolding Simple_WPC_def pushout_step_def
[PROOF STATE]
proof (prove)
using this:
set_of_graph_rules Rs \<and> (\<forall>i. graph (S i) \<and> S i = S (Suc i) \<or> (\<exists>R\<in>Rs. subgraph (S i) (S (Suc i)) \<and> (\<exists>f\<^sub>1 f\<^sub>2. graph_homomorphism (fst R) (S i) f\<^sub>1 \<and> graph_homomorphism (snd R) (S (Suc i)) f\<^sub>2 \<and> f\<^sub>1 \<subseteq> f\<^sub>2 \<and> weak_universal t R (S i) (S (Suc i)) f\<^sub>1 f\<^sub>2)))

goal (1 subgoal):
 1. subgraph (S i) (S (Suc i))
[PROOF STEP]
by (cases "graph (S i) \<and> S i = S (Suc i)",auto)
[PROOF STATE]
proof (state)
this:
subgraph (S ?i) (S (Suc ?i))

goal (1 subgoal):
 1. chain S
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
subgraph (S ?i) (S (Suc ?i))

goal (1 subgoal):
 1. chain S
[PROOF STEP]
unfolding chain_def
[PROOF STATE]
proof (prove)
using this:
subgraph (S ?i) (S (Suc ?i))

goal (1 subgoal):
 1. \<forall>i. subgraph (S i) (S (i + 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
chain S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extensible_from_chainI:
  assumes ch:"chain S"
  and igh:"graph_homomorphism (S 0) C f"
  and ind:"\<And> f i. graph_homomorphism (S i) C f \<Longrightarrow>
                \<exists>h. (graph_homomorphism (S (Suc i)) C h) \<and> agree_on (S i) f h"
  shows "extensible (S 0,chain_sup S) C f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
have ch:"chain S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
chain S
graph_homomorphism (S 0) C f
graph_homomorphism (S ?i) C ?f \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc ?i)) C h \<and> agree_on (S ?i) ?f h

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

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
hence r0:"\<exists>x. graph_homomorphism (S 0) C x \<and> (0 = 0 \<longrightarrow> x = f)"
[PROOF STATE]
proof (prove)
using this:
chain S

goal (1 subgoal):
 1. \<exists>x. graph_homomorphism (S 0) C x \<and> ((0::'d) = (0::'d) \<longrightarrow> x = f)
[PROOF STEP]
using igh
[PROOF STATE]
proof (prove)
using this:
chain S
graph_homomorphism (S 0) C f

goal (1 subgoal):
 1. \<exists>x. graph_homomorphism (S 0) C x \<and> ((0::'d) = (0::'d) \<longrightarrow> x = f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. graph_homomorphism (S 0) C x \<and> ((0::?'d1) = (0::?'d1) \<longrightarrow> x = f)

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<exists>x. graph_homomorphism (S 0) C x \<and> ((0::?'d1) = (0::?'d1) \<longrightarrow> x = f)

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
fix i x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
assume "graph_homomorphism (S i) C x \<and> (i = 0 \<longrightarrow> x = f)"
[PROOF STATE]
proof (state)
this:
graph_homomorphism (S i) C x \<and> (i = 0 \<longrightarrow> x = f)

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
hence "graph_homomorphism (S i) C x"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (S i) C x \<and> (i = 0 \<longrightarrow> x = f)

goal (1 subgoal):
 1. graph_homomorphism (S i) C x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (S i) C x

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
from ind[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
have "\<exists>y. (graph_homomorphism (S (Suc i)) C y \<and> (Suc i = 0 \<longrightarrow> y = f)) \<and> agree_on (S i) x y"
[PROOF STATE]
proof (prove)
using this:
\<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h

goal (1 subgoal):
 1. \<exists>y. (graph_homomorphism (S (Suc i)) C y \<and> (Suc i = 0 \<longrightarrow> y = f)) \<and> agree_on (S i) x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. (graph_homomorphism (S (Suc i)) C y \<and> (Suc i = 0 \<longrightarrow> y = f)) \<and> agree_on (S i) x y

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
graph_homomorphism (S ?i3) C ?x3 \<and> (?i3 = 0 \<longrightarrow> ?x3 = f) \<Longrightarrow> \<exists>y. (graph_homomorphism (S (Suc ?i3)) C y \<and> (Suc ?i3 = 0 \<longrightarrow> y = f)) \<and> agree_on (S ?i3) ?x3 y

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
with r0
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. graph_homomorphism (S 0) C x \<and> ((0::?'d1) = (0::?'d1) \<longrightarrow> x = f)
graph_homomorphism (S ?i3) C ?x3 \<and> (?i3 = 0 \<longrightarrow> ?x3 = f) \<Longrightarrow> \<exists>y. (graph_homomorphism (S (Suc ?i3)) C y \<and> (Suc ?i3 = 0 \<longrightarrow> y = f)) \<and> agree_on (S ?i3) ?x3 y
[PROOF STEP]
have "\<exists> g. (\<forall> i. (graph_homomorphism (S i) C (g i) \<and> (i = 0 \<longrightarrow> g i = f))
                \<and> agree_on (S i) (g i) (g (Suc i)) )"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. graph_homomorphism (S 0) C x \<and> ((0::?'d1) = (0::?'d1) \<longrightarrow> x = f)
graph_homomorphism (S ?i3) C ?x3 \<and> (?i3 = 0 \<longrightarrow> ?x3 = f) \<Longrightarrow> \<exists>y. (graph_homomorphism (S (Suc ?i3)) C y \<and> (Suc ?i3 = 0 \<longrightarrow> y = f)) \<and> agree_on (S ?i3) ?x3 y

goal (1 subgoal):
 1. \<exists>g. \<forall>i. (graph_homomorphism (S i) C (g i) \<and> (i = 0 \<longrightarrow> g i = f)) \<and> agree_on (S i) (g i) (g (Suc i))
[PROOF STEP]
by (rule dependent_nat_choice)
[PROOF STATE]
proof (state)
this:
\<exists>g. \<forall>i. (graph_homomorphism (S i) C (g i) \<and> (i = 0 \<longrightarrow> g i = f)) \<and> agree_on (S i) (g i) (g (Suc i))

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g. \<forall>i. (graph_homomorphism (S i) C (g i) \<and> (i = 0 \<longrightarrow> g i = f)) \<and> agree_on (S i) (g i) (g (Suc i))
[PROOF STEP]
obtain g where
       mtn:"g 0 = f"
           "graph_homomorphism (S i) C (g i)"
           "agree_on (S i) (g i) (g (i + 1))" for i
[PROOF STATE]
proof (prove)
using this:
\<exists>g. \<forall>i. (graph_homomorphism (S i) C (g i) \<and> (i = 0 \<longrightarrow> g i = f)) \<and> agree_on (S i) (g i) (g (Suc i))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g 0 = f; \<And>i. graph_homomorphism (S i) C (g i); \<And>i. agree_on (S i) (g i) (g (i + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g 0 = f
graph_homomorphism (S ?i1) C (g ?i1)
agree_on (S ?i1) (g ?i1) (g (?i1 + 1))

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
from extend_for_chain[OF mtn ch]
[PROOF STATE]
proof (chain)
picking this:
extensible (S 0, chain_sup S) C f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extensible (S 0, chain_sup S) C f

goal (1 subgoal):
 1. extensible (S 0, chain_sup S) C f
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
extensible (S 0, chain_sup S) C f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wpc_least:
  assumes "WPC (t:: 'x itself) Rs S"
  shows "least t Rs (S 0) (chain_sup S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least t Rs (S 0) (chain_sup S)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
WPC t Rs S

goal (1 subgoal):
 1. least t Rs (S 0) (chain_sup S)
[PROOF STEP]
proof(induction S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t Rs S. Simple_WPC t Rs S \<Longrightarrow> least t Rs (S 0) (chain_sup S)
 2. \<And>S t Rs. \<lbrakk>chain S; \<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')\<rbrakk> \<Longrightarrow> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
case (wpc_simpl t Rs S)
[PROOF STATE]
proof (state)
this:
Simple_WPC t Rs S

goal (2 subgoals):
 1. \<And>t Rs S. Simple_WPC t Rs S \<Longrightarrow> least t Rs (S 0) (chain_sup S)
 2. \<And>S t Rs. \<lbrakk>chain S; \<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')\<rbrakk> \<Longrightarrow> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
hence gr:"set_of_graph_rules Rs"
    and ps:"\<And> i. S i = S (Suc i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S i) (S (i + 1)))"
[PROOF STATE]
proof (prove)
using this:
Simple_WPC t Rs S

goal (1 subgoal):
 1. set_of_graph_rules Rs &&& (\<And>i. S i = S (Suc i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S i) (S (i + 1))))
[PROOF STEP]
unfolding Simple_WPC_def
[PROOF STATE]
proof (prove)
using this:
set_of_graph_rules Rs \<and> (\<forall>i. graph (S i) \<and> S i = S (Suc i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S i) (S (Suc i))))

goal (1 subgoal):
 1. set_of_graph_rules Rs &&& (\<And>i. S i = S (Suc i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S i) (S (i + 1))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_of_graph_rules Rs
S ?i = S (Suc ?i) \<or> (\<exists>R\<in>Rs. pushout_step t R (S ?i) (S (?i + 1)))

goal (2 subgoals):
 1. \<And>t Rs S. Simple_WPC t Rs S \<Longrightarrow> least t Rs (S 0) (chain_sup S)
 2. \<And>S t Rs. \<lbrakk>chain S; \<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')\<rbrakk> \<Longrightarrow> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
have ch[intro]:"chain S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain S
[PROOF STEP]
using wpc_simpl
[PROOF STATE]
proof (prove)
using this:
Simple_WPC t Rs S

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

goal (2 subgoals):
 1. \<And>t Rs S. Simple_WPC t Rs S \<Longrightarrow> least t Rs (S 0) (chain_sup S)
 2. \<And>S t Rs. \<lbrakk>chain S; \<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')\<rbrakk> \<Longrightarrow> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least t Rs (S 0) (chain_sup S)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subgraph (S 0) (chain_sup S)
 2. \<And>C. consequence_graph Rs C \<Longrightarrow> maintained (S 0, chain_sup S) C
[PROOF STEP]
fix C::"('a,'x) labeled_graph"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subgraph (S 0) (chain_sup S)
 2. \<And>C. consequence_graph Rs C \<Longrightarrow> maintained (S 0, chain_sup S) C
[PROOF STEP]
assume cgC:"consequence_graph Rs C"
[PROOF STATE]
proof (state)
this:
consequence_graph Rs C

goal (2 subgoals):
 1. subgraph (S 0) (chain_sup S)
 2. \<And>C. consequence_graph Rs C \<Longrightarrow> maintained (S 0, chain_sup S) C
[PROOF STEP]
show "maintained (S 0, chain_sup S) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (S 0, chain_sup S) C
[PROOF STEP]
proof(standard,rule extensible_from_chainI,goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
 3. \<And>f fa i. \<lbrakk>graph_homomorphism (S 0) C f; graph_homomorphism (S i) C fa\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) fa h
[PROOF STEP]
case (3 f x i)
[PROOF STATE]
proof (state)
this:
graph_homomorphism (S 0) C f
graph_homomorphism (S i) C x

goal (3 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
 3. \<And>f fa i. \<lbrakk>graph_homomorphism (S 0) C f; graph_homomorphism (S i) C fa\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) fa h
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
proof(cases "S i = S (Suc i)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S i = S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
 2. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
S i = S (Suc i)

goal (2 subgoals):
 1. S i = S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
 2. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (S 0) C f
graph_homomorphism (S i) C x
S i = S (Suc i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (S 0) C f
graph_homomorphism (S i) C x
S i = S (Suc i)

goal (1 subgoal):
 1. \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h

goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
S i \<noteq> S (Suc i)

goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
with ps[of i,unfolded pushout_step_def]
[PROOF STATE]
proof (chain)
picking this:
S i = S (Suc i) \<or> (\<exists>R\<in>Rs. subgraph (S i) (S (i + 1)) \<and> (\<exists>f\<^sub>1 f\<^sub>2. graph_homomorphism (fst R) (S i) f\<^sub>1 \<and> graph_homomorphism (snd R) (S (i + 1)) f\<^sub>2 \<and> f\<^sub>1 \<subseteq> f\<^sub>2 \<and> weak_universal t R (S i) (S (i + 1)) f\<^sub>1 f\<^sub>2))
S i \<noteq> S (Suc i)
[PROOF STEP]
obtain R f\<^sub>1 f\<^sub>2 where
        R:"(fst R,snd R) \<in> Rs" and f\<^sub>1:"graph_homomorphism (fst R) (S i) f\<^sub>1"
        and wu:"weak_universal t R (S i) (S (i + 1)) f\<^sub>1 f\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
S i = S (Suc i) \<or> (\<exists>R\<in>Rs. subgraph (S i) (S (i + 1)) \<and> (\<exists>f\<^sub>1 f\<^sub>2. graph_homomorphism (fst R) (S i) f\<^sub>1 \<and> graph_homomorphism (snd R) (S (i + 1)) f\<^sub>2 \<and> f\<^sub>1 \<subseteq> f\<^sub>2 \<and> weak_universal t R (S i) (S (i + 1)) f\<^sub>1 f\<^sub>2))
S i \<noteq> S (Suc i)

goal (1 subgoal):
 1. (\<And>R f\<^sub>1 f\<^sub>2. \<lbrakk>(fst R, snd R) \<in> Rs; graph_homomorphism (fst R) (S i) f\<^sub>1; weak_universal t R (S i) (S (i + 1)) f\<^sub>1 f\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(fst R, snd R) \<in> Rs
graph_homomorphism (fst R) (S i) f\<^sub>1
weak_universal t R (S i) (S (i + 1)) f\<^sub>1 f\<^sub>2

goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
from graph_homomorphism_composes[OF f\<^sub>1 3(2)]
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (fst R) C (f\<^sub>1 O x)
[PROOF STEP]
have ih_comp:"graph_homomorphism (fst R) C (f\<^sub>1 O x)"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst R) C (f\<^sub>1 O x)

goal (1 subgoal):
 1. graph_homomorphism (fst R) C (f\<^sub>1 O x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
graph_homomorphism (fst R) C (f\<^sub>1 O x)

goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
with maintainedD[OF consequence_graphD(1)[OF cgC R]]
[PROOF STATE]
proof (chain)
picking this:
graph_homomorphism (fst R) C ?f \<Longrightarrow> extensible (fst R, snd R) C ?f
graph_homomorphism (fst R) C (f\<^sub>1 O x)
[PROOF STEP]
have "extensible (fst R, snd R) C (f\<^sub>1 O x)"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (fst R) C ?f \<Longrightarrow> extensible (fst R, snd R) C ?f
graph_homomorphism (fst R) C (f\<^sub>1 O x)

goal (1 subgoal):
 1. extensible (fst R, snd R) C (f\<^sub>1 O x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extensible (fst R, snd R) C (f\<^sub>1 O x)

goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
from this[unfolded extensible_def prod.sel]
[PROOF STATE]
proof (chain)
picking this:
\<exists>g. graph_homomorphism (snd R) C g \<and> agree_on (fst R) (f\<^sub>1 O x) g
[PROOF STEP]
obtain g where g:"graph_homomorphism (snd R) C g" "f\<^sub>1 O x \<subseteq> g"
[PROOF STATE]
proof (prove)
using this:
\<exists>g. graph_homomorphism (snd R) C g \<and> agree_on (fst R) (f\<^sub>1 O x) g

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>graph_homomorphism (snd R) C g; f\<^sub>1 O x \<subseteq> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using agree_iff_subset[OF ih_comp]
[PROOF STATE]
proof (prove)
using this:
\<exists>g. graph_homomorphism (snd R) C g \<and> agree_on (fst R) (f\<^sub>1 O x) g
univalent ?g \<Longrightarrow> agree_on (fst R) (f\<^sub>1 O x) ?g = (f\<^sub>1 O x \<subseteq> ?g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>graph_homomorphism (snd R) C g; f\<^sub>1 O x \<subseteq> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding graph_homomorphism_def
[PROOF STATE]
proof (prove)
using this:
\<exists>g. (vertices (snd R) = Domain g \<and> graph (snd R) \<and> graph C \<and> g `` vertices (snd R) \<subseteq> vertices C \<and> univalent g \<and> edge_preserving g (edges (snd R)) (edges C)) \<and> agree_on (fst R) (f\<^sub>1 O x) g
univalent ?g \<Longrightarrow> agree_on (fst R) (f\<^sub>1 O x) ?g = (f\<^sub>1 O x \<subseteq> ?g)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>vertices (snd R) = Domain g \<and> graph (snd R) \<and> graph C \<and> g `` vertices (snd R) \<subseteq> vertices C \<and> univalent g \<and> edge_preserving g (edges (snd R)) (edges C); f\<^sub>1 O x \<subseteq> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (snd R) C g
f\<^sub>1 O x \<subseteq> g

goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
from weak_universalD[OF wu g(1) 3(2) g(2)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>h. graph_homomorphism (S (i + 1)) C h \<and> x \<subseteq> h
[PROOF STEP]
obtain h where
          h:"graph_homomorphism (S (i + 1)) C h" "x \<subseteq> h"
[PROOF STATE]
proof (prove)
using this:
\<exists>h. graph_homomorphism (S (i + 1)) C h \<and> x \<subseteq> h

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>graph_homomorphism (S (i + 1)) C h; x \<subseteq> h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
graph_homomorphism (S (i + 1)) C h
x \<subseteq> h

goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
hence "agree_on (S i) x h"
[PROOF STATE]
proof (prove)
using this:
graph_homomorphism (S (i + 1)) C h
x \<subseteq> h

goal (1 subgoal):
 1. agree_on (S i) x h
[PROOF STEP]
by(subst agree_iff_subset[OF 3(2)], auto simp:graph_homomorphism_def)
[PROOF STATE]
proof (state)
this:
agree_on (S i) x h

goal (1 subgoal):
 1. S i \<noteq> S (Suc i) \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
agree_on (S i) x h
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
agree_on (S i) x h

goal (1 subgoal):
 1. \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
using h(1)
[PROOF STATE]
proof (prove)
using this:
agree_on (S i) x h
graph_homomorphism (S (i + 1)) C h

goal (1 subgoal):
 1. \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) x h

goal (2 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
maintained (S 0, chain_sup S) C

goal (1 subgoal):
 1. subgraph (S 0) (chain_sup S)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
least t Rs (S 0) (chain_sup S)

goal (1 subgoal):
 1. \<And>S t Rs. \<lbrakk>chain S; \<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')\<rbrakk> \<Longrightarrow> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S t Rs. \<lbrakk>chain S; \<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')\<rbrakk> \<Longrightarrow> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
case (wpc_combo S t Rs)
[PROOF STATE]
proof (state)
this:
chain S
\<exists>S'. S' 0 = S ?i \<and> chain_sup S' = S (Suc ?i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')

goal (1 subgoal):
 1. \<And>S t Rs. \<lbrakk>chain S; \<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')\<rbrakk> \<Longrightarrow> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
hence ps:"\<And> i. \<exists>S'. S' 0 = S i \<and>
         chain_sup S' = S (Suc i) \<and>
         WPC t Rs S' \<and>
         least t Rs (S' 0) (chain_sup S')"
    and ch[intro]:"chain S"
[PROOF STATE]
proof (prove)
using this:
chain S
\<exists>S'. S' 0 = S ?i \<and> chain_sup S' = S (Suc ?i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')

goal (1 subgoal):
 1. (\<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')) &&& chain S
[PROOF STEP]
unfolding Simple_WPC_def
[PROOF STATE]
proof (prove)
using this:
chain S
\<exists>S'. S' 0 = S ?i \<and> chain_sup S' = S (Suc ?i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')

goal (1 subgoal):
 1. (\<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')) &&& chain S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>S'. S' 0 = S ?i \<and> chain_sup S' = S (Suc ?i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')
chain S

goal (1 subgoal):
 1. \<And>S t Rs. \<lbrakk>chain S; \<And>i. \<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')\<rbrakk> \<Longrightarrow> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least t Rs (S 0) (chain_sup S)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subgraph (S 0) (chain_sup S)
 2. \<And>C. consequence_graph Rs C \<Longrightarrow> maintained (S 0, chain_sup S) C
[PROOF STEP]
fix C :: "('a, 'x) labeled_graph"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. subgraph (S 0) (chain_sup S)
 2. \<And>C. consequence_graph Rs C \<Longrightarrow> maintained (S 0, chain_sup S) C
[PROOF STEP]
assume cgC:"consequence_graph Rs C"
[PROOF STATE]
proof (state)
this:
consequence_graph Rs C

goal (2 subgoals):
 1. subgraph (S 0) (chain_sup S)
 2. \<And>C. consequence_graph Rs C \<Longrightarrow> maintained (S 0, chain_sup S) C
[PROOF STEP]
show "maintained (S 0, chain_sup S) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maintained (S 0, chain_sup S) C
[PROOF STEP]
proof(standard,rule extensible_from_chainI,goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
 3. \<And>f fa i. \<lbrakk>graph_homomorphism (S 0) C f; graph_homomorphism (S i) C fa\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) fa h
[PROOF STEP]
case (3 f g i)
[PROOF STATE]
proof (state)
this:
graph_homomorphism (S 0) C f
graph_homomorphism (S i) C g

goal (3 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
 3. \<And>f fa i. \<lbrakk>graph_homomorphism (S 0) C f; graph_homomorphism (S i) C fa\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) fa h
[PROOF STEP]
from ps[of i]
[PROOF STATE]
proof (chain)
picking this:
\<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')
[PROOF STEP]
have "least t Rs (S i) (S (Suc i))"
[PROOF STATE]
proof (prove)
using this:
\<exists>S'. S' 0 = S i \<and> chain_sup S' = S (Suc i) \<and> WPC t Rs S' \<and> least t Rs (S' 0) (chain_sup S')

goal (1 subgoal):
 1. least t Rs (S i) (S (Suc i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
least t Rs (S i) (S (Suc i))

goal (3 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
 3. \<And>f fa i. \<lbrakk>graph_homomorphism (S 0) C f; graph_homomorphism (S i) C fa\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) fa h
[PROOF STEP]
with cgC
[PROOF STATE]
proof (chain)
picking this:
consequence_graph Rs C
least t Rs (S i) (S (Suc i))
[PROOF STEP]
have ss:"subgraph (S i) (S (Suc i))" "maintained (S i, S (Suc i)) C"
[PROOF STATE]
proof (prove)
using this:
consequence_graph Rs C
least t Rs (S i) (S (Suc i))

goal (1 subgoal):
 1. subgraph (S i) (S (Suc i)) &&& maintained (S i, S (Suc i)) C
[PROOF STEP]
unfolding least_def
[PROOF STATE]
proof (prove)
using this:
consequence_graph Rs C
subgraph (S i) (S (Suc i)) \<and> (\<forall>C. consequence_graph Rs C \<longrightarrow> maintained (S i, S (Suc i)) C)

goal (1 subgoal):
 1. subgraph (S i) (S (Suc i)) &&& maintained (S i, S (Suc i)) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgraph (S i) (S (Suc i))
maintained (S i, S (Suc i)) C

goal (3 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
 3. \<And>f fa i. \<lbrakk>graph_homomorphism (S 0) C f; graph_homomorphism (S i) C fa\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) fa h
[PROOF STEP]
from ss(2) 3(2)
[PROOF STATE]
proof (chain)
picking this:
maintained (S i, S (Suc i)) C
graph_homomorphism (S i) C g
[PROOF STEP]
have "extensible (S i, S (Suc i)) C g"
[PROOF STATE]
proof (prove)
using this:
maintained (S i, S (Suc i)) C
graph_homomorphism (S i) C g

goal (1 subgoal):
 1. extensible (S i, S (Suc i)) C g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extensible (S i, S (Suc i)) C g

goal (3 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
 3. \<And>f fa i. \<lbrakk>graph_homomorphism (S 0) C f; graph_homomorphism (S i) C fa\<rbrakk> \<Longrightarrow> \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) fa h
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extensible (S i, S (Suc i)) C g

goal (1 subgoal):
 1. \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) g h
[PROOF STEP]
unfolding extensible_def prod.sel
[PROOF STATE]
proof (prove)
using this:
\<exists>ga. graph_homomorphism (S (Suc i)) C ga \<and> agree_on (S i) g ga

goal (1 subgoal):
 1. \<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) g h
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>h. graph_homomorphism (S (Suc i)) C h \<and> agree_on (S i) g h

goal (2 subgoals):
 1. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> chain S
 2. \<And>f. graph_homomorphism (S 0) C f \<Longrightarrow> graph_homomorphism (S 0) C f
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
maintained (S 0, chain_sup S) C

goal (1 subgoal):
 1. subgraph (S 0) (chain_sup S)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
least t Rs (S 0) (chain_sup S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wpc_least_consequence_graph:
  assumes "WPC t Rs S" "consequence_graph Rs (chain_sup S)"
  shows "least_consequence_graph t Rs (S 0) (chain_sup S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_consequence_graph t Rs (S 0) (chain_sup S)
[PROOF STEP]
using wpc_least assms
[PROOF STATE]
proof (prove)
using this:
WPC ?t ?Rs ?S \<Longrightarrow> least ?t ?Rs (?S 0) (chain_sup ?S)
WPC t Rs S
consequence_graph Rs (chain_sup S)

goal (1 subgoal):
 1. least_consequence_graph t Rs (S 0) (chain_sup S)
[PROOF STEP]
unfolding least_consequence_graph_def
[PROOF STATE]
proof (prove)
using this:
WPC ?t ?Rs ?S \<Longrightarrow> least ?t ?Rs (?S 0) (chain_sup ?S)
WPC t Rs S
consequence_graph Rs (chain_sup S)

goal (1 subgoal):
 1. consequence_graph Rs (chain_sup S) \<and> least t Rs (S 0) (chain_sup S)
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsplit_lemma: "(maxsplit P res ps qs = (xs,ys)) =
  (if \<exists>us. prefix us qs \<and> P(ps@us) then xs@ys=ps@qs \<and> is_maxpref P xs (ps@qs)
   else (xs,ys)=res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (maxsplit P res ps qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P (ps @ us) then xs @ ys = ps @ qs \<and> is_maxpref P xs (ps @ qs) else (xs, ys) = res)
[PROOF STEP]
proof (induction P res ps qs rule: maxsplit.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P res ps. (maxsplit P res ps [] = (xs, ys)) = (if \<exists>us. prefix us [] \<and> P (ps @ us) then xs @ ys = ps @ [] \<and> is_maxpref P xs (ps @ []) else (xs, ys) = res)
 2. \<And>P res ps q qs. (maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res)) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>P res ps. (maxsplit P res ps [] = (xs, ys)) = (if \<exists>us. prefix us [] \<and> P (ps @ us) then xs @ ys = ps @ [] \<and> is_maxpref P xs (ps @ []) else (xs, ys) = res)
 2. \<And>P res ps q qs. (maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res)) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (maxsplit P_ res_ ps_ [] = (xs, ys)) = (if \<exists>us. prefix us [] \<and> P_ (ps_ @ us) then xs @ ys = ps_ @ [] \<and> is_maxpref P_ xs (ps_ @ []) else (xs, ys) = res_)
[PROOF STEP]
by (auto simp: is_maxpref_def split: if_splits)
[PROOF STATE]
proof (state)
this:
(maxsplit P_ res_ ps_ [] = (xs, ys)) = (if \<exists>us. prefix us [] \<and> P_ (ps_ @ us) then xs @ ys = ps_ @ [] \<and> is_maxpref P_ xs (ps_ @ []) else (xs, ys) = res_)

goal (1 subgoal):
 1. \<And>P res ps q qs. (maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res)) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P res ps q qs. (maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res)) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
case (2 P res ps q qs)
[PROOF STATE]
proof (state)
this:
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))

goal (1 subgoal):
 1. \<And>P res ps q qs. (maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res)) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
proof (cases "\<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
case ex1: True
[PROOF STATE]
proof (state)
this:
\<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us)

goal (2 subgoals):
 1. \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us)
[PROOF STEP]
obtain us where "prefix us qs" "P ((ps @ [q]) @ us)"
[PROOF STATE]
proof (prove)
using this:
\<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us)

goal (1 subgoal):
 1. (\<And>us. \<lbrakk>prefix us qs; P ((ps @ [q]) @ us)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prefix us qs
P ((ps @ [q]) @ us)

goal (2 subgoals):
 1. \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
hence ex2: "\<exists>us. prefix us (q # qs) \<and> P (ps @ us)"
[PROOF STATE]
proof (prove)
using this:
prefix us qs
P ((ps @ [q]) @ us)

goal (1 subgoal):
 1. \<exists>us. prefix us (q # qs) \<and> P (ps @ us)
[PROOF STEP]
by (intro exI[of _ "q#us"]) auto
[PROOF STATE]
proof (state)
this:
\<exists>us. prefix us (q # qs) \<and> P (ps @ us)

goal (2 subgoals):
 1. \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
with ex1 and 2
[PROOF STATE]
proof (chain)
picking this:
\<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us)
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))
\<exists>us. prefix us (q # qs) \<and> P (ps @ us)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us)
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))
\<exists>us. prefix us (q # qs) \<and> P (ps @ us)

goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)

goal (1 subgoal):
 1. \<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
case ex1: False
[PROOF STATE]
proof (state)
this:
\<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us)

goal (1 subgoal):
 1. \<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
proof (cases "\<exists>us. prefix us (q#qs) \<and> P (ps @ us)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>us. prefix us (q # qs) \<and> P (ps @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<nexists>us. prefix us (q # qs) \<and> P (ps @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>us. prefix us (q # qs) \<and> P (ps @ us)

goal (2 subgoals):
 1. \<exists>us. prefix us (q # qs) \<and> P (ps @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<nexists>us. prefix us (q # qs) \<and> P (ps @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))

goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
by (simp only: ex1 False) (insert ex1 False, auto simp: prefix_Cons)
[PROOF STATE]
proof (state)
this:
(maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)

goal (1 subgoal):
 1. \<exists>us. prefix us (q # qs) \<and> P (ps @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>us. prefix us (q # qs) \<and> P (ps @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>us. prefix us (q # qs) \<and> P (ps @ us)

goal (1 subgoal):
 1. \<exists>us. prefix us (q # qs) \<and> P (ps @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
note ex2 = this
[PROOF STATE]
proof (state)
this:
\<exists>us. prefix us (q # qs) \<and> P (ps @ us)

goal (1 subgoal):
 1. \<exists>us. prefix us (q # qs) \<and> P (ps @ us) \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
proof (cases "P ps")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
P ps

goal (2 subgoals):
 1. P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))
P ps
[PROOF STEP]
have "(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) \<longleftrightarrow> (xs = ps \<and> ys = q # qs)"
[PROOF STATE]
proof (prove)
using this:
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))
P ps

goal (1 subgoal):
 1. (maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) = (xs = ps \<and> ys = q # qs)
[PROOF STEP]
by (simp only: ex1 ex2) simp_all
[PROOF STATE]
proof (state)
this:
(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) = (xs = ps \<and> ys = q # qs)

goal (2 subgoals):
 1. P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) = (xs = ps \<and> ys = q # qs)

goal (2 subgoals):
 1. P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs = ps \<and> ys = q # qs) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))
[PROOF STEP]
using ex1 True
[PROOF STATE]
proof (prove)
using this:
\<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us)
P ps

goal (1 subgoal):
 1. (xs = ps \<and> ys = q # qs) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))
[PROOF STEP]
by (auto simp: is_maxpref_def prefix_append prefix_Cons append_eq_append_conv2)
[PROOF STATE]
proof (state)
this:
(xs = ps \<and> ys = q # qs) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))

goal (2 subgoals):
 1. P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
 2. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))

goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
(maxsplit P (ps, q # qs) (ps @ [q]) qs = (xs, ys)) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))
P ps

goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
by (simp only: ex1 ex2) simp_all
[PROOF STATE]
proof (state)
this:
(maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)

goal (1 subgoal):
 1. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> P ps

goal (1 subgoal):
 1. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))
\<not> P ps
[PROOF STEP]
have "(maxsplit P res (ps @ [q]) qs = (xs, ys)) \<longleftrightarrow> ((xs, ys) = res)"
[PROOF STATE]
proof (prove)
using this:
(maxsplit P (if P ps then (ps, q # qs) else res) (ps @ [q]) qs = (xs, ys)) = (if \<exists>us. prefix us qs \<and> P ((ps @ [q]) @ us) then xs @ ys = (ps @ [q]) @ qs \<and> is_maxpref P xs ((ps @ [q]) @ qs) else (xs, ys) = (if P ps then (ps, q # qs) else res))
\<not> P ps

goal (1 subgoal):
 1. (maxsplit P res (ps @ [q]) qs = (xs, ys)) = ((xs, ys) = res)
[PROOF STEP]
by (simp only: ex1 ex2) simp
[PROOF STATE]
proof (state)
this:
(maxsplit P res (ps @ [q]) qs = (xs, ys)) = ((xs, ys) = res)

goal (1 subgoal):
 1. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(maxsplit P res (ps @ [q]) qs = (xs, ys)) = ((xs, ys) = res)

goal (1 subgoal):
 1. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
have "\<dots> \<longleftrightarrow> (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((xs, ys) = res) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))
[PROOF STEP]
using ex1 ex2 False
[PROOF STATE]
proof (prove)
using this:
\<nexists>us. prefix us qs \<and> P ((ps @ [q]) @ us)
\<exists>us. prefix us (q # qs) \<and> P (ps @ us)
\<not> P ps

goal (1 subgoal):
 1. ((xs, ys) = res) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))
[PROOF STEP]
by (auto simp: append_eq_append_conv2 is_maxpref_def prefix_Cons)
[PROOF STATE]
proof (state)
this:
((xs, ys) = res) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))

goal (1 subgoal):
 1. \<not> P ps \<Longrightarrow> (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(maxsplit P res (ps @ [q]) qs = (xs, ys)) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(maxsplit P res (ps @ [q]) qs = (xs, ys)) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))

goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
(maxsplit P res (ps @ [q]) qs = (xs, ys)) = (xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs))
\<not> P ps

goal (1 subgoal):
 1. (maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)
[PROOF STEP]
by (simp only: ex1 ex2) simp
[PROOF STATE]
proof (state)
this:
(maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(maxsplit P res ps (q # qs) = (xs, ys)) = (if \<exists>us. prefix us (q # qs) \<and> P (ps @ us) then xs @ ys = ps @ q # qs \<and> is_maxpref P xs (ps @ q # qs) else (xs, ys) = res)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_maxpref_Nil[simp]:
 "\<not>(\<exists>us. prefix us xs \<and> P us) \<Longrightarrow> is_maxpref P ps xs = (ps = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>us. prefix us xs \<and> P us \<Longrightarrow> is_maxpref P ps xs = (ps = [])
[PROOF STEP]
by (auto simp: is_maxpref_def)


[STATEMENT]
lemma is_maxsplitter_maxsplit:
 "is_maxsplitter P (\<lambda>xs. maxsplit P ([],xs) [] xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_maxsplitter P (\<lambda>xs. maxsplit P ([], xs) [] xs)
[PROOF STEP]
by (auto simp: maxsplit_lemma is_maxsplitter_def)


[STATEMENT]
lemma pred_unfold:
  "pred n = n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred n = n - 1
[PROOF STEP]
by (induct n) simp_all


[STATEMENT]
lemma fermat:
  assumes "prime p" "m mod p \<noteq> 0"
  shows "m^(p-(1::nat)) mod p = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m ^ (p - 1) mod p = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m ^ (p - 1) mod p = 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
prime p
m mod p \<noteq> 0
[PROOF STEP]
have "[m ^ (p - 1) = 1] (mod p)"
[PROOF STATE]
proof (prove)
using this:
prime p
m mod p \<noteq> 0

goal (1 subgoal):
 1. [m ^ (p - 1) = 1] (mod p)
[PROOF STEP]
using fermat_theorem [of p m]
[PROOF STATE]
proof (prove)
using this:
prime p
m mod p \<noteq> 0
\<lbrakk>prime p; \<not> p dvd m\<rbrakk> \<Longrightarrow> [m ^ (p - 1) = 1] (mod p)

goal (1 subgoal):
 1. [m ^ (p - 1) = 1] (mod p)
[PROOF STEP]
by (simp add: mod_eq_0_iff_dvd)
[PROOF STATE]
proof (state)
this:
[m ^ (p - 1) = 1] (mod p)

goal (1 subgoal):
 1. m ^ (p - 1) mod p = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[m ^ (p - 1) = 1] (mod p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[m ^ (p - 1) = 1] (mod p)

goal (1 subgoal):
 1. m ^ (p - 1) mod p = 1
[PROOF STEP]
using \<open>prime p\<close> prime_gt_1_nat [of p]
[PROOF STATE]
proof (prove)
using this:
[m ^ (p - 1) = 1] (mod p)
prime p
prime p \<Longrightarrow> 1 < p

goal (1 subgoal):
 1. m ^ (p - 1) mod p = 1
[PROOF STEP]
by (simp add: cong_def)
[PROOF STATE]
proof (state)
this:
m ^ (p - 1) mod p = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cryptinverts_hilf1: "prime p \<Longrightarrow> (m * m ^(k * pred p)) mod p = m mod p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> m * m ^ (k * pred p) mod p = m mod p
[PROOF STEP]
apply (cases "m mod p = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prime p; m mod p = 0\<rbrakk> \<Longrightarrow> m * m ^ (k * pred p) mod p = m mod p
 2. \<lbrakk>prime p; m mod p \<noteq> 0\<rbrakk> \<Longrightarrow> m * m ^ (k * pred p) mod p = m mod p
[PROOF STEP]
apply (simp add: mod_mult_left_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prime p; m mod p = 0\<rbrakk> \<Longrightarrow> m * m ^ (k * pred p) mod p = 0
 2. \<lbrakk>prime p; m mod p \<noteq> 0\<rbrakk> \<Longrightarrow> m * m ^ (k * pred p) mod p = m mod p
[PROOF STEP]
apply (simp only: mult.commute [of k "pred p"]
    power_mult mod_mult_right_eq [of "m" "(m^pred p)^k" "p"]
    remainderexp [of "m^pred p" "p" "k", symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prime p; m mod p = 0\<rbrakk> \<Longrightarrow> m * (m ^ pred p) ^ k mod p = 0
 2. \<lbrakk>prime p; m mod p \<noteq> 0\<rbrakk> \<Longrightarrow> m * m ^ (k * pred p) mod p = m mod p
[PROOF STEP]
apply (insert fermat [of p m], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; 0 < m mod p; m ^ (p - Suc 0) mod p = Suc 0\<rbrakk> \<Longrightarrow> m * m ^ (k * pred p) mod p = m mod p
[PROOF STEP]
apply (simp add: mult.commute [of k] power_mult pred_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; 0 < m mod p; m ^ (p - Suc 0) mod p = Suc 0\<rbrakk> \<Longrightarrow> m * (m ^ (p - Suc 0)) ^ k mod p = m mod p
[PROOF STEP]
by (metis One_nat_def mod_mult_right_eq mult.right_neutral power_Suc_0 power_mod)


[STATEMENT]
lemma cryptinverts_hilf2: "prime p \<Longrightarrow> m*(m^(k * (pred p) * (pred q))) mod p = m mod p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> m * m ^ (k * pred p * pred q) mod p = m mod p
[PROOF STEP]
apply (simp add: mult.commute [of "k * pred p" "pred q"] mult.assoc [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> m * m ^ (pred q * k * pred p) mod p = m mod p
[PROOF STEP]
apply (rule cryptinverts_hilf1 [of "p" "m" "(pred q) * k"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> prime p
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cryptinverts_hilf3: "prime q \<Longrightarrow> m*(m^(k * (pred p) * (pred q))) mod q = m mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime q \<Longrightarrow> m * m ^ (k * pred p * pred q) mod q = m mod q
[PROOF STEP]
by (fact cryptinverts_hilf1)


[STATEMENT]
lemma cryptinverts_hilf4:
  "m ^ x mod (p * q) = m" if "prime p" "prime q" "p \<noteq> q"
    "m < p * q" "x mod (pred p * pred q) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m ^ x mod (p * q) = m
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> m ^ x mod (p * q) = m
 2. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> m ^ x mod (p * q) = m
 2. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
prime p
prime q
p \<noteq> q
m < p * q
x mod (pred p * pred q) = 1
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime p
prime q
p \<noteq> q
m < p * q
x mod (pred p * pred q) = 1
x = 0

goal (1 subgoal):
 1. m ^ x mod (p * q) = m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m ^ x mod (p * q) = m

goal (1 subgoal):
 1. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
x = Suc x

goal (1 subgoal):
 1. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
with that(5)
[PROOF STATE]
proof (chain)
picking this:
x mod (pred p * pred q) = 1
x = Suc x
[PROOF STEP]
have "Suc x mod (pred p * pred q) = Suc 0"
[PROOF STATE]
proof (prove)
using this:
x mod (pred p * pred q) = 1
x = Suc x

goal (1 subgoal):
 1. Suc x mod (pred p * pred q) = Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc x mod (pred p * pred q) = Suc 0

goal (1 subgoal):
 1. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc x mod (pred p * pred q) = Suc 0
[PROOF STEP]
have "pred p * pred q dvd x"
[PROOF STATE]
proof (prove)
using this:
Suc x mod (pred p * pred q) = Suc 0

goal (1 subgoal):
 1. pred p * pred q dvd x
[PROOF STEP]
using dvd_minus_mod [of "(pred p * pred q)" "Suc x"]
[PROOF STATE]
proof (prove)
using this:
Suc x mod (pred p * pred q) = Suc 0
pred p * pred q dvd Suc x - Suc x mod (pred p * pred q)

goal (1 subgoal):
 1. pred p * pred q dvd x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pred p * pred q dvd x

goal (1 subgoal):
 1. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pred p * pred q dvd x
[PROOF STEP]
obtain y where "x = pred p * pred q * y"
[PROOF STATE]
proof (prove)
using this:
pred p * pred q dvd x

goal (1 subgoal):
 1. (\<And>y. x = pred p * pred q * y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x = pred p * pred q * y

goal (1 subgoal):
 1. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = pred p * pred q * y
[PROOF STEP]
have "m ^ Suc x mod p = m mod p" and "m ^ Suc x mod q = m mod q"
[PROOF STATE]
proof (prove)
using this:
x = pred p * pred q * y

goal (1 subgoal):
 1. m ^ Suc x mod p = m mod p &&& m ^ Suc x mod q = m mod q
[PROOF STEP]
using cryptinverts_hilf2 [of p m y q, OF \<open>prime p\<close>]
      cryptinverts_hilf3 [of q m y p, OF \<open>prime q\<close>]
[PROOF STATE]
proof (prove)
using this:
x = pred p * pred q * y
m * m ^ (y * pred p * pred q) mod p = m mod p
m * m ^ (y * pred p * pred q) mod q = m mod q

goal (1 subgoal):
 1. m ^ Suc x mod p = m mod p &&& m ^ Suc x mod q = m mod q
[PROOF STEP]
by (simp_all add: ac_simps)
[PROOF STATE]
proof (state)
this:
m ^ Suc x mod p = m mod p
m ^ Suc x mod q = m mod q

goal (1 subgoal):
 1. \<And>nat. x = Suc nat \<Longrightarrow> m ^ x mod (p * q) = m
[PROOF STEP]
with that Suc
[PROOF STATE]
proof (chain)
picking this:
prime p
prime q
p \<noteq> q
m < p * q
x mod (pred p * pred q) = 1
x = Suc x
m ^ Suc x mod p = m mod p
m ^ Suc x mod q = m mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime p
prime q
p \<noteq> q
m < p * q
x mod (pred p * pred q) = 1
x = Suc x
m ^ Suc x mod p = m mod p
m ^ Suc x mod q = m mod q

goal (1 subgoal):
 1. m ^ x mod (p * q) = m
[PROOF STEP]
by (auto intro: specializedtoprimes1a)
[PROOF STATE]
proof (state)
this:
m ^ x mod (p * q) = m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primmultgreater: fixes p::nat shows "\<lbrakk> prime p; prime q; p \<noteq> 2; q \<noteq> 2\<rbrakk> \<Longrightarrow> 2 < p*q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> 2; q \<noteq> 2\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply (simp add: prime_nat_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc 0 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = Suc 0 \<or> m = p); Suc 0 < q \<and> (\<forall>m. m dvd q \<longrightarrow> m = Suc 0 \<or> m = q); p \<noteq> 2; q \<noteq> 2\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply (insert mult_le_mono [of 2 p 2 q])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc 0 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = Suc 0 \<or> m = p); Suc 0 < q \<and> (\<forall>m. m dvd q \<longrightarrow> m = Suc 0 \<or> m = q); p \<noteq> 2; q \<noteq> 2; \<lbrakk>2 \<le> p; 2 \<le> q\<rbrakk> \<Longrightarrow> 2 * 2 \<le> p * q\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma primmultgreater2: fixes p::nat shows "\<lbrakk>prime p; prime q; p \<noteq> q\<rbrakk> \<Longrightarrow>  2 < p*q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply (cases "p = 2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; p = 2\<rbrakk> \<Longrightarrow> 2 < p * q
 2. \<lbrakk>prime p; prime q; p \<noteq> q; p \<noteq> 2\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prime q; q \<noteq> 2; p = 2\<rbrakk> \<Longrightarrow> Suc 0 < q
 2. \<lbrakk>prime p; prime q; p \<noteq> q; p \<noteq> 2\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply (simp add: prime_nat_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; p \<noteq> 2\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply (cases "q = 2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; p \<noteq> 2; q = 2\<rbrakk> \<Longrightarrow> 2 < p * q
 2. \<lbrakk>prime p; prime q; p \<noteq> q; p \<noteq> 2; q \<noteq> 2\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply (simp add: prime_nat_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; p \<noteq> 2; q \<noteq> 2\<rbrakk> \<Longrightarrow> 2 < p * q
[PROOF STEP]
apply (erule primmultgreater)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>prime q; p \<noteq> q; p \<noteq> 2; q \<noteq> 2\<rbrakk> \<Longrightarrow> prime q
 2. \<lbrakk>prime q; p \<noteq> q; p \<noteq> 2; q \<noteq> 2\<rbrakk> \<Longrightarrow> p \<noteq> 2
 3. \<lbrakk>prime q; p \<noteq> q; p \<noteq> 2; q \<noteq> 2\<rbrakk> \<Longrightarrow> q \<noteq> 2
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cryptinverts: "\<lbrakk> prime p; prime q; p \<noteq> q; n = p*q; m < n;
    e*d mod ((pred p)*(pred q)) = 1\<rbrakk> \<Longrightarrow> rsa_crypt (rsa_crypt m e n) d n = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; m < n; e * d mod (pred p * pred q) = 1\<rbrakk> \<Longrightarrow> rsa_crypt (rsa_crypt m e n) d n = m
[PROOF STEP]
apply (insert cryptinverts_hilf4 [of p q m "e*d"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; m < n; e * d mod (pred p * pred q) = 1; \<lbrakk>prime p; prime q; p \<noteq> q; m < p * q; e * d mod (pred p * pred q) = 1\<rbrakk> \<Longrightarrow> m ^ (e * d) mod (p * q) = m\<rbrakk> \<Longrightarrow> rsa_crypt (rsa_crypt m e n) d n = m
[PROOF STEP]
apply (insert cryptcorrect [of "p*q" "rsa_crypt m e (p * q)" d])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; m < n; e * d mod (pred p * pred q) = 1; \<lbrakk>prime p; prime q; p \<noteq> q; m < p * q; e * d mod (pred p * pred q) = 1\<rbrakk> \<Longrightarrow> m ^ (e * d) mod (p * q) = m; rsa_crypt (p * q) (rsa_crypt m e (p * q)) d = (p * q) ^ rsa_crypt m e (p * q) mod d\<rbrakk> \<Longrightarrow> rsa_crypt (rsa_crypt m e n) d n = m
[PROOF STEP]
apply (insert cryptcorrect [of "p*q" m e])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; m < n; e * d mod (pred p * pred q) = 1; \<lbrakk>prime p; prime q; p \<noteq> q; m < p * q; e * d mod (pred p * pred q) = 1\<rbrakk> \<Longrightarrow> m ^ (e * d) mod (p * q) = m; rsa_crypt (p * q) (rsa_crypt m e (p * q)) d = (p * q) ^ rsa_crypt m e (p * q) mod d; rsa_crypt (p * q) m e = (p * q) ^ m mod e\<rbrakk> \<Longrightarrow> rsa_crypt (rsa_crypt m e n) d n = m
[PROOF STEP]
apply (insert primmultgreater2 [of p q])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; m < n; e * d mod (pred p * pred q) = 1; \<lbrakk>prime p; prime q; p \<noteq> q; m < p * q; e * d mod (pred p * pred q) = 1\<rbrakk> \<Longrightarrow> m ^ (e * d) mod (p * q) = m; rsa_crypt (p * q) (rsa_crypt m e (p * q)) d = (p * q) ^ rsa_crypt m e (p * q) mod d; rsa_crypt (p * q) m e = (p * q) ^ m mod e; \<lbrakk>prime p; prime q; p \<noteq> q\<rbrakk> \<Longrightarrow> 2 < p * q\<rbrakk> \<Longrightarrow> rsa_crypt (rsa_crypt m e n) d n = m
[PROOF STEP]
apply (simp add: prime_nat_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc 0 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = Suc 0 \<or> m = p); Suc 0 < q \<and> (\<forall>m. m dvd q \<longrightarrow> m = Suc 0 \<or> m = q); p \<noteq> q; n = p * q; m < p * q; e * d mod (pred p * pred q) = Suc 0; m ^ (e * d) mod (p * q) = m; rsa_crypt (p * q) (rsa_crypt m e (p * q)) d = (p * q) ^ rsa_crypt m e (p * q) mod d; rsa_crypt (p * q) m e = (p * q) ^ m mod e; 2 < p * q\<rbrakk> \<Longrightarrow> rsa_crypt (rsa_crypt m e (p * q)) d (p * q) = m
[PROOF STEP]
apply (simp add: cryptcorrect remainderexp [of "m^e" "p*q" d] power_mult [symmetric])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma simpler_gets_def: "gets f = (\<lambda>s. ({(f s, s)}, False))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gets f = (\<lambda>s. ({(f s, s)}, False))
[PROOF STEP]
apply (simp add: gets_def return_def bind_def get_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma simpler_modify_def:
  "modify f = (\<lambda>s. ({((), f s)}, False))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. modify f = (\<lambda>s. ({((), f s)}, False))
[PROOF STEP]
by (simp add: modify_def bind_def get_def put_def)


[STATEMENT]
lemma bind_def':
  "(f >>= g) \<equiv>
       \<lambda>s. ({(r'', s''). \<exists>(r', s') \<in> fst (f s). (r'', s'') \<in> fst (g r' s') },
                     snd (f s) \<or> (\<exists>(r', s') \<in> fst (f s). snd (g r' s')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f >>= g \<equiv> \<lambda>s. ({(r'', s''). \<exists>(r', s')\<in>fst (f s). (r'', s'') \<in> fst (g r' s')}, snd (f s) \<or> (\<exists>(r', s')\<in>fst (f s). snd (g r' s')))
[PROOF STEP]
apply (rule eq_reflection)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f >>= g = (\<lambda>s. ({(r'', s''). \<exists>(r', s')\<in>fst (f s). (r'', s'') \<in> fst (g r' s')}, snd (f s) \<or> (\<exists>(r', s')\<in>fst (f s). snd (g r' s'))))
[PROOF STEP]
apply (auto simp add: bind_def split_def Let_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma return_bind [simp]: "(return x >>= f) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return x >>= f = f x
[PROOF STEP]
by (simp add: return_def bind_def)


[STATEMENT]
lemma bind_return [simp]: "(m >>= return) = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m >>= return = m
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (m >>= return) x = m x
[PROOF STEP]
apply (simp add: bind_def return_def split_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bind_assoc:
  fixes m :: "('a,'b) nondet_monad"
  fixes f :: "'b \<Rightarrow> ('a,'c) nondet_monad"
  fixes g :: "'c \<Rightarrow> ('a,'d) nondet_monad"
  shows "(m >>= f) >>= g  =  m >>= (\<lambda>x. f x >>= g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m >>= f >>= g = m >>= (\<lambda>x. f x >>= g)
[PROOF STEP]
apply (unfold bind_def Let_def split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s)) \<or> snd (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s)))) = (\<lambda>s. (\<Union> (fst ` (\<lambda>p. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p)) \<or> snd (f (fst p) (snd p)))) ` fst (m s)), True \<in> snd ` (\<lambda>p. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p)) \<or> snd (f (fst p) (snd p)))) ` fst (m s) \<or> snd (m s)))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s)) \<or> snd (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s))) = (\<Union> (fst ` (\<lambda>p. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p)) \<or> snd (f (fst p) (snd p)))) ` fst (m s)), True \<in> snd ` (\<lambda>p. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p)) \<or> snd (f (fst p) (snd p)))) ` fst (m s) \<or> snd (m s))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<exists>y\<in>fst (m s). \<exists>x\<in>fst (f (fst y) (snd y)). snd (g (fst x) (snd x))) \<or> (\<exists>x\<in>fst (m s). snd (f (fst x) (snd x))) \<or> snd (m s)) = ((\<exists>x\<in>fst (m s). (\<exists>x\<in>fst (f (fst x) (snd x)). snd (g (fst x) (snd x))) \<or> snd (f (fst x) (snd x))) \<or> snd (m s))
[PROOF STEP]
apply (auto intro: rev_image_eqI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma liftE_def2:
  "liftE f = (\<lambda>s. ((\<lambda>(v,s'). (Inr v, s')) ` fst (f s), snd (f s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftE f = (\<lambda>s. ((\<lambda>(v, s'). (Inr v, s')) ` fst (f s), snd (f s)))
[PROOF STEP]
by (auto simp: liftE_def return_def split_def bind_def)


[STATEMENT]
lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. returnOk x >>=E f = f x
[PROOF STEP]
apply (simp only: bindE_def return_def returnOk_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> Inr) x >>= lift f = f x
[PROOF STEP]
apply (clarsimp simp: lift_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lift_return [simp]:
  "lift (return \<circ> Inr) = return"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift (return \<circ> Inr) = return
[PROOF STEP]
by (rule ext)
     (simp add: lift_def throwError_def split: sum.splits)


[STATEMENT]
lemma bindE_returnOk [simp]: "(m >>=E returnOk) = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m >>=E returnOk = m
[PROOF STEP]
by (simp add: bindE_def returnOk_def)


[STATEMENT]
lemma bindE_assoc:
  "(m >>=E f) >>=E g = m >>=E (\<lambda>x. f x >>=E g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m >>=E f >>=E g = m >>=E (\<lambda>x. f x >>=E g)
[PROOF STEP]
apply (simp add: bindE_def bind_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m >>= (\<lambda>x. lift f x >>= lift g) = m >>= lift (\<lambda>x. f x >>= lift g)
[PROOF STEP]
apply (rule arg_cong [where f="\<lambda>x. m >>= x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. lift f x >>= lift g) = lift (\<lambda>x. f x >>= lift g)
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. lift f x >>= lift g = lift (\<lambda>x. f x >>= lift g) x
[PROOF STEP]
apply (case_tac x, simp_all add: lift_def throwError_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma returnOk_liftE:
  "returnOk x = liftE (return x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. returnOk x = liftE (return x)
[PROOF STEP]
by (simp add: liftE_def returnOk_def)


[STATEMENT]
lemma throwError_bindE [simp]:
  "(throwError E >>=E f) = throwError E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. throwError E >>=E f = throwError E
[PROOF STEP]
by (simp add: bindE_def bind_def throwError_def lift_def return_def)


[STATEMENT]
lemma "do x \<leftarrow> return 1;
          return (2::nat);
          return x
       od =
       return 1 >>=
       (\<lambda>x. return (2::nat) >>=
            K_bind (return x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. do x \<leftarrow> return (1::'b);
return 2;
return x
od = do x \<leftarrow> return (1::'b);
return 2;
return x
od
[PROOF STEP]
by (rule refl)


[STATEMENT]
lemma "do x \<leftarrow> return 1;
          return 2;
          return x
       od = return 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. do x \<leftarrow> return (1::'b);
return (2::'c);
return x
od = return (1::'b)
[PROOF STEP]
by simp