[STATEMENT]
lemma rcp_spec_f4_red: "rcp_spec f4_red"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rcp_spec f4_red
[PROOF STEP]
proof (rule rcp_specI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>gs bs ps sps data. 0 \<notin> fst ` set (fst (f4_red gs bs ps sps data))
 2. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 3. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 5. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat \<times> 'd"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>gs bs ps sps data. 0 \<notin> fst ` set (fst (f4_red gs bs ps sps data))
 2. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 3. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 5. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
show "0 \<notin> fst ` set (fst (f4_red gs bs ps sps data))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> fst ` set (fst (f4_red gs bs ps sps data))
[PROOF STEP]
by (simp add: fst_set_fst_f4_red f4_red_aux_not_zero)
[PROOF STATE]
proof (state)
this:
0 \<notin> fst ` set (fst (f4_red gs bs ps sps data))

goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps h b and data::"nat \<times> 'd"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
assume "h \<in> set (fst (f4_red gs bs ps sps data))" and "b \<in> set gs \<union> set bs"
[PROOF STATE]
proof (state)
this:
h \<in> set (fst (f4_red gs bs ps sps data))
b \<in> set gs \<union> set bs

goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
h \<in> set (fst (f4_red gs bs ps sps data))
[PROOF STEP]
have "fst h \<in> fst ` set (fst (f4_red gs bs ps sps data))"
[PROOF STATE]
proof (prove)
using this:
h \<in> set (fst (f4_red gs bs ps sps data))

goal (1 subgoal):
 1. fst h \<in> fst ` set (fst (f4_red gs bs ps sps data))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst h \<in> fst ` set (fst (f4_red gs bs ps sps data))

goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
hence "fst h \<in> set (f4_red_aux (gs @ bs) sps)"
[PROOF STATE]
proof (prove)
using this:
fst h \<in> fst ` set (fst (f4_red gs bs ps sps data))

goal (1 subgoal):
 1. fst h \<in> set (f4_red_aux (gs @ bs) sps)
[PROOF STEP]
by (simp only: fst_set_fst_f4_red)
[PROOF STATE]
proof (state)
this:
fst h \<in> set (f4_red_aux (gs @ bs) sps)

goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst h \<in> set (f4_red_aux (gs @ bs) sps)

goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
from \<open>b \<in> set gs \<union> set bs\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<in> set gs \<union> set bs
[PROOF STEP]
have "b \<in> set (gs @ bs)"
[PROOF STATE]
proof (prove)
using this:
b \<in> set gs \<union> set bs

goal (1 subgoal):
 1. b \<in> set (gs @ bs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b \<in> set (gs @ bs)

goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
b \<in> set (gs @ bs)

goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
assume "fst b \<noteq> 0"
[PROOF STATE]
proof (state)
this:
fst b \<noteq> 0

goal (4 subgoals):
 1. \<And>gs bs ps sps h b data. \<lbrakk>h \<in> set (fst (f4_red gs bs ps sps data)); b \<in> set gs \<union> set bs; fst b \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> lt (fst b) adds\<^sub>t lt (fst h)
 2. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 4. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst h \<in> set (f4_red_aux (gs @ bs) sps)
b \<in> set (gs @ bs)
fst b \<noteq> 0
[PROOF STEP]
show "\<not> lt (fst b) adds\<^sub>t lt (fst h)"
[PROOF STATE]
proof (prove)
using this:
fst h \<in> set (f4_red_aux (gs @ bs) sps)
b \<in> set (gs @ bs)
fst b \<noteq> 0

goal (1 subgoal):
 1. \<not> lt (fst b) adds\<^sub>t lt (fst h)
[PROOF STEP]
by (rule f4_red_aux_irredudible)
[PROOF STATE]
proof (state)
this:
\<not> lt (fst b) adds\<^sub>t lt (fst h)

goal (3 subgoals):
 1. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and d::"'a \<Rightarrow> nat" and data::"nat \<times> 'd"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
assume "dickson_grading d"
[PROOF STATE]
proof (state)
this:
dickson_grading d

goal (3 subgoals):
 1. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
hence "dgrad_p_set_le d (set (f4_red_aux (gs @ bs) sps)) (args_to_set ([], gs @ bs, sps))"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

goal (1 subgoal):
 1. dgrad_p_set_le d (set (f4_red_aux (gs @ bs) sps)) (args_to_set ([], gs @ bs, sps))
[PROOF STEP]
by (fact f4_red_aux_dgrad_p_set_le)
[PROOF STATE]
proof (state)
this:
dgrad_p_set_le d (set (f4_red_aux (gs @ bs) sps)) (args_to_set ([], gs @ bs, sps))

goal (3 subgoals):
 1. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dgrad_p_set_le d (set (f4_red_aux (gs @ bs) sps)) (args_to_set ([], gs @ bs, sps))

goal (3 subgoals):
 1. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
have "... = args_to_set (gs, bs, sps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. args_to_set ([], gs @ bs, sps) = args_to_set (gs, bs, sps)
[PROOF STEP]
by (simp add: args_to_set_alt image_Un)
[PROOF STATE]
proof (state)
this:
args_to_set ([], gs @ bs, sps) = args_to_set (gs, bs, sps)

goal (3 subgoals):
 1. \<And>gs bs ps sps d data. dickson_grading d \<Longrightarrow> dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 3. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dgrad_p_set_le d (set (f4_red_aux (gs @ bs) sps)) (args_to_set (gs, bs, sps))
[PROOF STEP]
show "dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))"
[PROOF STATE]
proof (prove)
using this:
dgrad_p_set_le d (set (f4_red_aux (gs @ bs) sps)) (args_to_set (gs, bs, sps))

goal (1 subgoal):
 1. dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))
[PROOF STEP]
by (simp only: fst_set_fst_f4_red)
[PROOF STATE]
proof (state)
this:
dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))

goal (2 subgoals):
 1. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat \<times> 'd"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
have "component_of_term ` Keys (set (f4_red_aux (gs @ bs) sps)) \<subseteq>
        component_of_term ` Keys (args_to_set ([], gs @ bs, sps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (set (f4_red_aux (gs @ bs) sps)) \<subseteq> component_of_term ` Keys (args_to_set ([], gs @ bs, sps))
[PROOF STEP]
by (fact components_f4_red_aux_subset)
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (f4_red_aux (gs @ bs) sps)) \<subseteq> component_of_term ` Keys (args_to_set ([], gs @ bs, sps))

goal (2 subgoals):
 1. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (set (f4_red_aux (gs @ bs) sps)) \<subseteq> component_of_term ` Keys (args_to_set ([], gs @ bs, sps))

goal (2 subgoals):
 1. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
have "... = component_of_term ` Keys (args_to_set (gs, bs, sps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. component_of_term ` Keys (args_to_set ([], gs @ bs, sps)) = component_of_term ` Keys (args_to_set (gs, bs, sps))
[PROOF STEP]
by (simp add: args_to_set_alt image_Un)
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (args_to_set ([], gs @ bs, sps)) = component_of_term ` Keys (args_to_set (gs, bs, sps))

goal (2 subgoals):
 1. \<And>gs bs ps sps data. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
 2. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
component_of_term ` Keys (set (f4_red_aux (gs @ bs) sps)) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
[PROOF STEP]
show "component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq>
        component_of_term ` Keys (args_to_set (gs, bs, sps))"
[PROOF STATE]
proof (prove)
using this:
component_of_term ` Keys (set (f4_red_aux (gs @ bs) sps)) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))

goal (1 subgoal):
 1. component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))
[PROOF STEP]
by (simp only: fst_set_fst_f4_red)
[PROOF STATE]
proof (state)
this:
component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) \<subseteq> component_of_term ` Keys (args_to_set (gs, bs, sps))

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat \<times> 'd"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
have "set (f4_red_aux (gs @ bs) sps) \<subseteq> pmdl (args_to_set ([], gs @ bs, sps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (f4_red_aux (gs @ bs) sps) \<subseteq> pmdl (args_to_set ([], gs @ bs, sps))
[PROOF STEP]
by (fact pmdl_f4_red_aux)
[PROOF STATE]
proof (state)
this:
set (f4_red_aux (gs @ bs) sps) \<subseteq> pmdl (args_to_set ([], gs @ bs, sps))

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (f4_red_aux (gs @ bs) sps) \<subseteq> pmdl (args_to_set ([], gs @ bs, sps))

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
have "... = pmdl (args_to_set (gs, bs, sps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (args_to_set ([], gs @ bs, sps)) = pmdl (args_to_set (gs, bs, sps))
[PROOF STEP]
by (simp add: args_to_set_alt image_Un)
[PROOF STATE]
proof (state)
this:
pmdl (args_to_set ([], gs @ bs, sps)) = pmdl (args_to_set (gs, bs, sps))

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (f4_red_aux (gs @ bs) sps) \<subseteq> pmdl (args_to_set (gs, bs, sps))
[PROOF STEP]
have "fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps))"
[PROOF STATE]
proof (prove)
using this:
set (f4_red_aux (gs @ bs) sps) \<subseteq> pmdl (args_to_set (gs, bs, sps))

goal (1 subgoal):
 1. fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps))
[PROOF STEP]
by (simp only: fst_set_fst_f4_red)
[PROOF STATE]
proof (state)
this:
fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps))

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps))

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps))

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
fix p q :: "('t, 'b, 'c) pdata"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
assume "set sps \<subseteq> set bs \<times> (set gs \<union> set bs)"
[PROOF STATE]
proof (state)
this:
set sps \<subseteq> set bs \<times> (set gs \<union> set bs)

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
hence "set sps \<subseteq> set (gs @ bs) \<times> set (gs @ bs)"
[PROOF STATE]
proof (prove)
using this:
set sps \<subseteq> set bs \<times> (set gs \<union> set bs)

goal (1 subgoal):
 1. set sps \<subseteq> set (gs @ bs) \<times> set (gs @ bs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set sps \<subseteq> set (gs @ bs) \<times> set (gs @ bs)

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set sps \<subseteq> set (gs @ bs) \<times> set (gs @ bs)

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
assume "(p, q) \<in> set sps"
[PROOF STATE]
proof (state)
this:
(p, q) \<in> set sps

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set sps \<subseteq> set (gs @ bs) \<times> set (gs @ bs)
(p, q) \<in> set sps
[PROOF STEP]
have "(red (fst ` set (gs @ bs) \<union> set (f4_red_aux (gs @ bs) sps)))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0"
[PROOF STATE]
proof (prove)
using this:
set sps \<subseteq> set (gs @ bs) \<times> set (gs @ bs)
(p, q) \<in> set sps

goal (1 subgoal):
 1. (red (fst ` set (gs @ bs) \<union> set (f4_red_aux (gs @ bs) sps)))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0
[PROOF STEP]
by (rule f4_red_aux_spoly_reducible)
[PROOF STATE]
proof (state)
this:
(red (fst ` set (gs @ bs) \<union> set (f4_red_aux (gs @ bs) sps)))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>set sps \<subseteq> set bs \<times> (set gs \<union> set bs); (?p106, ?q106) \<in> set sps\<rbrakk> \<Longrightarrow> (red (fst ` set (gs @ bs) \<union> set (f4_red_aux (gs @ bs) sps)))\<^sup>*\<^sup>* (spoly (fst ?p106) (fst ?q106)) 0

goal (1 subgoal):
 1. \<And>gs bs ps sps data. \<lbrakk>is_Groebner_basis (fst ` set gs); unique_idx (gs @ bs) data\<rbrakk> \<Longrightarrow> fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps))
\<lbrakk>set sps \<subseteq> set bs \<times> (set gs \<union> set bs); (?p106, ?q106) \<in> set sps\<rbrakk> \<Longrightarrow> (red (fst ` set (gs @ bs) \<union> set (f4_red_aux (gs @ bs) sps)))\<^sup>*\<^sup>* (spoly (fst ?p106) (fst ?q106)) 0
[PROOF STEP]
show
    "fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and>
     (\<forall>(p, q)\<in>set sps.
         set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow>
         (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)"
[PROOF STATE]
proof (prove)
using this:
fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps))
\<lbrakk>set sps \<subseteq> set bs \<times> (set gs \<union> set bs); (?p106, ?q106) \<in> set sps\<rbrakk> \<Longrightarrow> (red (fst ` set (gs @ bs) \<union> set (f4_red_aux (gs @ bs) sps)))\<^sup>*\<^sup>* (spoly (fst ?p106) (fst ?q106)) 0

goal (1 subgoal):
 1. fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)
[PROOF STEP]
by (auto simp add: image_Un fst_set_fst_f4_red)
[PROOF STATE]
proof (state)
this:
fst ` set (fst (f4_red gs bs ps sps data)) \<subseteq> pmdl (args_to_set (gs, bs, sps)) \<and> (\<forall>(p, q)\<in>set sps. set sps \<subseteq> set bs \<times> (set gs \<union> set bs) \<longrightarrow> (red (fst ` (set gs \<union> set bs) \<union> fst ` set (fst (f4_red gs bs ps sps data))))\<^sup>*\<^sup>* (spoly (fst p) (fst q)) 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f4_sel_aux_subset: "set (f4_sel_aux t ps) \<subseteq> set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (f4_sel_aux t ps) \<subseteq> set ps
[PROOF STEP]
by (induct ps, auto)


[STATEMENT]
lemma sel_spec_f4_sel: "sel_spec f4_sel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sel_spec f4_sel
[PROOF STEP]
proof (rule sel_specI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>gs bs ps data. ps \<noteq> [] \<Longrightarrow> f4_sel gs bs ps data \<noteq> [] \<and> set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
fix gs bs :: "('t, 'b, 'c) pdata list" and ps::"('t, 'b, 'c) pdata_pair list" and data::"nat \<times> 'd"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>gs bs ps data. ps \<noteq> [] \<Longrightarrow> f4_sel gs bs ps data \<noteq> [] \<and> set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
assume "ps \<noteq> []"
[PROOF STATE]
proof (state)
this:
ps \<noteq> []

goal (1 subgoal):
 1. \<And>gs bs ps data. ps \<noteq> [] \<Longrightarrow> f4_sel gs bs ps data \<noteq> [] \<and> set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ps \<noteq> []
[PROOF STEP]
obtain p ps' where ps: "ps = p # ps'"
[PROOF STATE]
proof (prove)
using this:
ps \<noteq> []

goal (1 subgoal):
 1. (\<And>p ps'. ps = p # ps' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson list.exhaust)
[PROOF STATE]
proof (state)
this:
ps = p # ps'

goal (1 subgoal):
 1. \<And>gs bs ps data. ps \<noteq> [] \<Longrightarrow> f4_sel gs bs ps data \<noteq> [] \<and> set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
show "f4_sel gs bs ps data \<noteq> [] \<and> set (f4_sel gs bs ps data) \<subseteq> set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f4_sel gs bs ps data \<noteq> [] \<and> set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f4_sel gs bs ps data \<noteq> []
 2. set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
show "f4_sel gs bs ps data \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f4_sel gs bs ps data \<noteq> []
[PROOF STEP]
by (simp add: ps)
[PROOF STATE]
proof (state)
this:
f4_sel gs bs ps data \<noteq> []

goal (1 subgoal):
 1. set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
from f4_sel_aux_subset
[PROOF STATE]
proof (chain)
picking this:
set (f4_sel_aux ?t ?ps) \<subseteq> set ?ps
[PROOF STEP]
show "set (f4_sel gs bs ps data) \<subseteq> set ps"
[PROOF STATE]
proof (prove)
using this:
set (f4_sel_aux ?t ?ps) \<subseteq> set ?ps

goal (1 subgoal):
 1. set (f4_sel gs bs ps data) \<subseteq> set ps
[PROOF STEP]
by (auto simp add: ps)
[PROOF STATE]
proof (state)
this:
set (f4_sel gs bs ps data) \<subseteq> set ps

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f4_sel gs bs ps data \<noteq> [] \<and> set (f4_sel gs bs ps data) \<subseteq> set ps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma struct_spec_f4: "struct_spec f4_sel add_pairs_canon add_basis_canon f4_red"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. struct_spec f4_sel add_pairs_canon add_basis_canon f4_red
[PROOF STEP]
using sel_spec_f4_sel ap_spec_add_pairs_canon ab_spec_add_basis_sorted compl_struct_f4_red
[PROOF STATE]
proof (prove)
using this:
sel_spec f4_sel
ap_spec add_pairs_canon
ab_spec (add_basis_sorted ?rel)
compl_struct f4_red

goal (1 subgoal):
 1. struct_spec f4_sel add_pairs_canon add_basis_canon f4_red
[PROOF STEP]
by (rule struct_specI)


[STATEMENT]
lemma (in gd_term) struct_spec_f4_punit: "punit.struct_spec punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. punit.struct_spec punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red
[PROOF STEP]
using punit.sel_spec_f4_sel ap_spec_add_pairs_punit_canon ab_spec_add_basis_sorted punit.compl_struct_f4_red
[PROOF STATE]
proof (prove)
using this:
sel_spec punit.f4_sel
punit.ap_spec add_pairs_punit_canon
ab_spec (add_basis_sorted ?rel)
punit.compl_struct punit.f4_red

goal (1 subgoal):
 1. punit.struct_spec punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red
[PROOF STEP]
by (rule punit.struct_specI)


[STATEMENT]
lemma "wf_list_graph G \<Longrightarrow> wf_graph (list_graph_to_graph G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_list_graph G \<Longrightarrow> wf_graph (list_graph_to_graph G)
[PROOF STEP]
by %invisible (metis wf_list_graph_def wf_list_graph_iff_wf_graph)


[STATEMENT]
lemma TopoS_eval_impl_proofrule:
    assumes inst: "SecurityInvariant sinvar_spec default_node_properties receiver_violation"
    assumes ev: "\<And>nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP"
    shows "
      (distinct (nodesL G) \<and> distinct (edgesL G) \<and>
       SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) =
      (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
proof (cases "wf_list_graph G")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
 2. \<not> wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
wf_list_graph G

goal (2 subgoals):
 1. wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
 2. \<not> wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
hence "sinvar_spec (list_graph_to_graph G) (SecurityInvariant.node_props default_node_properties P) =
       sinvar_impl G (SecurityInvariant.node_props default_node_properties P)"
[PROOF STATE]
proof (prove)
using this:
wf_list_graph G

goal (1 subgoal):
 1. sinvar_spec (list_graph_to_graph G) (SecurityInvariant.node_props default_node_properties P) = sinvar_impl G (SecurityInvariant.node_props default_node_properties P)
[PROOF STEP]
using ev
[PROOF STATE]
proof (prove)
using this:
wf_list_graph G
wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) ?nP = sinvar_impl G ?nP

goal (1 subgoal):
 1. sinvar_spec (list_graph_to_graph G) (SecurityInvariant.node_props default_node_properties P) = sinvar_impl G (SecurityInvariant.node_props default_node_properties P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sinvar_spec (list_graph_to_graph G) (SecurityInvariant.node_props default_node_properties P) = sinvar_impl G (SecurityInvariant.node_props default_node_properties P)

goal (2 subgoals):
 1. wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
 2. \<not> wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
with inst
[PROOF STATE]
proof (chain)
picking this:
SecurityInvariant sinvar_spec default_node_properties receiver_violation
sinvar_spec (list_graph_to_graph G) (SecurityInvariant.node_props default_node_properties P) = sinvar_impl G (SecurityInvariant.node_props default_node_properties P)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
SecurityInvariant sinvar_spec default_node_properties receiver_violation
sinvar_spec (list_graph_to_graph G) (SecurityInvariant.node_props default_node_properties P) = sinvar_impl G (SecurityInvariant.node_props default_node_properties P)

goal (1 subgoal):
 1. (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
unfolding wf_list_graph_def
[PROOF STATE]
proof (prove)
using this:
SecurityInvariant sinvar_spec default_node_properties receiver_violation
sinvar_spec (list_graph_to_graph G) (SecurityInvariant.node_props default_node_properties P) = sinvar_impl G (SecurityInvariant.node_props default_node_properties P)

goal (1 subgoal):
 1. (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = ((distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G) \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
by (simp add: wf_list_graph_iff_wf_graph SecurityInvariant.eval_def)
[PROOF STATE]
proof (state)
this:
(distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))

goal (1 subgoal):
 1. \<not> wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> wf_list_graph G

goal (1 subgoal):
 1. \<not> wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
hence "(distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G) = False"
[PROOF STATE]
proof (prove)
using this:
\<not> wf_list_graph G

goal (1 subgoal):
 1. (distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G) = False
[PROOF STEP]
unfolding wf_list_graph_def
[PROOF STATE]
proof (prove)
using this:
\<not> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G)

goal (1 subgoal):
 1. (distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G) = False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G) = False

goal (1 subgoal):
 1. \<not> wf_list_graph G \<Longrightarrow> (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> wf_list_graph G
(distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G) = False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> wf_list_graph G
(distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G) = False

goal (1 subgoal):
 1. (distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
unfolding SecurityInvariant.eval_def[OF inst]
[PROOF STATE]
proof (prove)
using this:
\<not> wf_list_graph G
(distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_list_graph_axioms G) = False

goal (1 subgoal):
 1. (distinct (nodesL G) \<and> distinct (edgesL G) \<and> wf_graph (list_graph_to_graph G) \<and> sinvar_spec (list_graph_to_graph G) (SecurityInvariant.node_props default_node_properties P)) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))
[PROOF STEP]
by (fastforce simp: wf_list_graph_iff_wf_graph)
[PROOF STATE]
proof (state)
this:
(distinct (nodesL G) \<and> distinct (edgesL G) \<and> SecurityInvariant.eval sinvar_spec default_node_properties (list_graph_to_graph G) P) = (wf_list_graph G \<and> sinvar_impl G (SecurityInvariant.node_props default_node_properties P))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Generic_offending_list_correct:
    assumes valid: "wf_list_graph G"
    assumes spec_impl: "\<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP"
    shows "SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP =
      set`set( Generic_offending_list sinvar_impl G nP )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
have "\<And> P G. set ` {x \<in> set (subseqs (edgesL G)). P G (set x)} = {x \<in> set ` set (subseqs (edgesL G)). P G (x)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P G. set ` {x \<in> set (subseqs (edgesL G)). P G (set x)} = {x \<in> set ` set (subseqs (edgesL G)). P G x}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set ` {x \<in> set (subseqs (edgesL ?G)). ?P ?G (set x)} = {x \<in> set ` set (subseqs (edgesL ?G)). ?P ?G x}

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
hence subset_subseqs_filter: "\<And> G P. {f. f \<subseteq> edges (list_graph_to_graph G) \<and> P G f}
    = set ` set [f\<leftarrow>subseqs (edgesL G) . P G (set f)]"
[PROOF STATE]
proof (prove)
using this:
set ` {x \<in> set (subseqs (edgesL ?G)). ?P ?G (set x)} = {x \<in> set ` set (subseqs (edgesL ?G)). ?P ?G x}

goal (1 subgoal):
 1. \<And>G P. {f. f \<subseteq> edges (list_graph_to_graph G) \<and> P G f} = set ` set (filter (\<lambda>f. P G (set f)) (subseqs (edgesL G)))
[PROOF STEP]
unfolding list_graph_to_graph_def
[PROOF STATE]
proof (prove)
using this:
set ` {x \<in> set (subseqs (edgesL ?G)). ?P ?G (set x)} = {x \<in> set ` set (subseqs (edgesL ?G)). ?P ?G x}

goal (1 subgoal):
 1. \<And>G P. {f. f \<subseteq> edges \<lparr>nodes = set (nodesL G), edges = set (edgesL G)\<rparr> \<and> P G f} = set ` set (filter (\<lambda>f. P G (set f)) (subseqs (edgesL G)))
[PROOF STEP]
by (auto simp: subseqs_powset)
[PROOF STATE]
proof (state)
this:
{f. f \<subseteq> edges (list_graph_to_graph ?G1) \<and> ?P1 ?G1 f} = set ` set (filter (\<lambda>f. ?P1 ?G1 (set f)) (subseqs (edgesL ?G1)))

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
from valid delete_edges_wf
[PROOF STATE]
proof (chain)
picking this:
wf_list_graph G
wf_list_graph ?G \<Longrightarrow> wf_list_graph (FiniteListGraph.delete_edges ?G ?E)
[PROOF STEP]
have "\<forall>f. wf_list_graph(FiniteListGraph.delete_edges G f)"
[PROOF STATE]
proof (prove)
using this:
wf_list_graph G
wf_list_graph ?G \<Longrightarrow> wf_list_graph (FiniteListGraph.delete_edges ?G ?E)

goal (1 subgoal):
 1. \<forall>f. wf_list_graph (FiniteListGraph.delete_edges G f)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>f. wf_list_graph (FiniteListGraph.delete_edges G f)

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
with spec_impl[symmetric] FiniteListGraph.delete_edges_correct[of "G"]
[PROOF STATE]
proof (chain)
picking this:
wf_list_graph ?G \<Longrightarrow> sinvar_impl ?G ?nP = sinvar_spec (list_graph_to_graph ?G) ?nP
FiniteGraph.delete_edges (list_graph_to_graph G) (set ?E) = list_graph_to_graph (FiniteListGraph.delete_edges G ?E)
\<forall>f. wf_list_graph (FiniteListGraph.delete_edges G f)
[PROOF STEP]
have impl_spec_delete:
      "\<forall>f. sinvar_impl (FiniteListGraph.delete_edges G f) nP =
          sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set f)) nP"
[PROOF STATE]
proof (prove)
using this:
wf_list_graph ?G \<Longrightarrow> sinvar_impl ?G ?nP = sinvar_spec (list_graph_to_graph ?G) ?nP
FiniteGraph.delete_edges (list_graph_to_graph G) (set ?E) = list_graph_to_graph (FiniteListGraph.delete_edges G ?E)
\<forall>f. wf_list_graph (FiniteListGraph.delete_edges G f)

goal (1 subgoal):
 1. \<forall>f. sinvar_impl (FiniteListGraph.delete_edges G f) nP = sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set f)) nP
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>f. sinvar_impl (FiniteListGraph.delete_edges G f) nP = sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set f)) nP

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
from spec_impl[OF valid, symmetric]
[PROOF STATE]
proof (chain)
picking this:
sinvar_impl G ?nP = sinvar_spec (list_graph_to_graph G) ?nP
[PROOF STEP]
have impl_spec_not:
      "(\<not> sinvar_impl G nP) = (\<not> sinvar_spec (list_graph_to_graph G) nP)"
[PROOF STATE]
proof (prove)
using this:
sinvar_impl G ?nP = sinvar_spec (list_graph_to_graph G) ?nP

goal (1 subgoal):
 1. (\<not> sinvar_impl G nP) = (\<not> sinvar_spec (list_graph_to_graph G) nP)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<not> sinvar_impl G nP) = (\<not> sinvar_spec (list_graph_to_graph G) nP)

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
from spec_impl[symmetric, OF FiniteListGraph.add_edge_wf[OF FiniteListGraph.delete_edges_wf[OF valid]]]
[PROOF STATE]
proof (chain)
picking this:
sinvar_impl (FiniteListGraph.add_edge ?v1 ?v'1 (FiniteListGraph.delete_edges G ?E2)) ?nP = sinvar_spec (list_graph_to_graph (FiniteListGraph.add_edge ?v1 ?v'1 (FiniteListGraph.delete_edges G ?E2))) ?nP
[PROOF STEP]
have impl_spec_allE:
    "\<forall> e1 e2 E. sinvar_impl (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G E)) nP =
    sinvar_spec (list_graph_to_graph (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G E))) nP"
[PROOF STATE]
proof (prove)
using this:
sinvar_impl (FiniteListGraph.add_edge ?v1 ?v'1 (FiniteListGraph.delete_edges G ?E2)) ?nP = sinvar_spec (list_graph_to_graph (FiniteListGraph.add_edge ?v1 ?v'1 (FiniteListGraph.delete_edges G ?E2))) ?nP

goal (1 subgoal):
 1. \<forall>e1 e2 E. sinvar_impl (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G E)) nP = sinvar_spec (list_graph_to_graph (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G E))) nP
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>e1 e2 E. sinvar_impl (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G E)) nP = sinvar_spec (list_graph_to_graph (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G E))) nP

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
have list_graph: "\<And> e1 e2 G f. (list_graph_to_graph (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G f))) =
      (FiniteGraph.add_edge e1 e2 (FiniteGraph.delete_edges (list_graph_to_graph G) (set f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e1 e2 G f. list_graph_to_graph (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G f)) = FiniteGraph.add_edge e1 e2 (FiniteGraph.delete_edges (list_graph_to_graph G) (set f))
[PROOF STEP]
by(simp add: FiniteListGraph.add_edge_correct FiniteListGraph.delete_edges_correct)
[PROOF STATE]
proof (state)
this:
list_graph_to_graph (FiniteListGraph.add_edge ?e1.2 ?e2.2 (FiniteListGraph.delete_edges ?G2 ?f2)) = FiniteGraph.add_edge ?e1.2 ?e2.2 (FiniteGraph.delete_edges (list_graph_to_graph ?G2) (set ?f2))

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)
[PROOF STEP]
unfolding SecurityInvariant_withOffendingFlows.set_offending_flows_def
      SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_def
      SecurityInvariant_withOffendingFlows.is_offending_flows_def
      Generic_offending_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {F. F \<subseteq> edges (list_graph_to_graph G) \<and> (\<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) F) nP) \<and> (\<forall>(e1, e2)\<in>F. \<not> sinvar_spec (FiniteGraph.add_edge e1 e2 (FiniteGraph.delete_edges (list_graph_to_graph G) F)) nP)} = set ` set (filter (\<lambda>f. (\<not> sinvar_impl G nP \<and> sinvar_impl (FiniteListGraph.delete_edges G f) nP) \<and> (\<forall>(e1, e2)\<in>set f. \<not> sinvar_impl (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G f)) nP)) (subseqs (edgesL G)))
[PROOF STEP]
apply(subst impl_spec_delete)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {F. F \<subseteq> edges (list_graph_to_graph G) \<and> (\<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) F) nP) \<and> (\<forall>(e1, e2)\<in>F. \<not> sinvar_spec (FiniteGraph.add_edge e1 e2 (FiniteGraph.delete_edges (list_graph_to_graph G) F)) nP)} = set ` set (filter (\<lambda>f. (\<not> sinvar_impl G nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set f)) nP) \<and> (\<forall>(e1, e2)\<in>set f. \<not> sinvar_impl (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G f)) nP)) (subseqs (edgesL G)))
[PROOF STEP]
apply(subst impl_spec_not)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {F. F \<subseteq> edges (list_graph_to_graph G) \<and> (\<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) F) nP) \<and> (\<forall>(e1, e2)\<in>F. \<not> sinvar_spec (FiniteGraph.add_edge e1 e2 (FiniteGraph.delete_edges (list_graph_to_graph G) F)) nP)} = set ` set (filter (\<lambda>f. (\<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set f)) nP) \<and> (\<forall>(e1, e2)\<in>set f. \<not> sinvar_impl (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G f)) nP)) (subseqs (edgesL G)))
[PROOF STEP]
apply(subst impl_spec_allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {F. F \<subseteq> edges (list_graph_to_graph G) \<and> (\<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) F) nP) \<and> (\<forall>(e1, e2)\<in>F. \<not> sinvar_spec (FiniteGraph.add_edge e1 e2 (FiniteGraph.delete_edges (list_graph_to_graph G) F)) nP)} = set ` set (filter (\<lambda>f. (\<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set f)) nP) \<and> (\<forall>(e1, e2)\<in>set f. \<not> sinvar_spec (list_graph_to_graph (FiniteListGraph.add_edge e1 e2 (FiniteListGraph.delete_edges G f))) nP)) (subseqs (edgesL G)))
[PROOF STEP]
apply(subst list_graph)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {F. F \<subseteq> edges (list_graph_to_graph G) \<and> (\<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) F) nP) \<and> (\<forall>(e1, e2)\<in>F. \<not> sinvar_spec (FiniteGraph.add_edge e1 e2 (FiniteGraph.delete_edges (list_graph_to_graph G) F)) nP)} = set ` set (filter (\<lambda>f. (\<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set f)) nP) \<and> (\<forall>(e1, e2)\<in>set f. \<not> sinvar_spec (FiniteGraph.add_edge e1 e2 (FiniteGraph.delete_edges (list_graph_to_graph G) (set f))) nP)) (subseqs (edgesL G)))
[PROOF STEP]
apply(rule subset_subseqs_filter)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP = set ` set (Generic_offending_list sinvar_impl G nP)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_edges_list_I: "P (list_graph_to_graph G) = Pl G \<Longrightarrow>
    (\<forall>(e1, e2)\<in> (edges (list_graph_to_graph G)). P (list_graph_to_graph G) e1 e2) = (\<forall>(e1, e2)\<in>set (edgesL G). Pl G e1 e2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (list_graph_to_graph G) = Pl G \<Longrightarrow> (\<forall>(e1, e2)\<in>edges (list_graph_to_graph G). P (list_graph_to_graph G) e1 e2) = (\<forall>(e1, e2)\<in>set (edgesL G). Pl G e1 e2)
[PROOF STEP]
unfolding list_graph_to_graph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<lparr>nodes = set (nodesL G), edges = set (edgesL G)\<rparr> = Pl G \<Longrightarrow> (\<forall>(e1, e2)\<in>edges \<lparr>nodes = set (nodesL G), edges = set (edgesL G)\<rparr>. P \<lparr>nodes = set (nodesL G), edges = set (edgesL G)\<rparr> e1 e2) = (\<forall>(e1, e2)\<in>set (edgesL G). Pl G e1 e2)
[PROOF STEP]
by simp


[STATEMENT]
lemma all_nodes_list_I: "P (list_graph_to_graph G) = Pl G \<Longrightarrow>
    (\<forall>n \<in> (nodes (list_graph_to_graph G)). P (list_graph_to_graph G) n) = (\<forall> n \<in>set (nodesL G). Pl G n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (list_graph_to_graph G) = Pl G \<Longrightarrow> (\<forall>n\<in>nodes (list_graph_to_graph G). P (list_graph_to_graph G) n) = (\<forall>n\<in>set (nodesL G). Pl G n)
[PROOF STEP]
unfolding list_graph_to_graph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<lparr>nodes = set (nodesL G), edges = set (edgesL G)\<rparr> = Pl G \<Longrightarrow> (\<forall>n\<in>nodes \<lparr>nodes = set (nodesL G), edges = set (edgesL G)\<rparr>. P \<lparr>nodes = set (nodesL G), edges = set (edgesL G)\<rparr> n) = (\<forall>n\<in>set (nodesL G). Pl G n)
[PROOF STEP]
by simp


[STATEMENT]
lemma minimalize_offending_overapprox_spec_impl:
    assumes valid: "wf_list_graph (G::'v::vertex list_graph)"
        and spec_impl: "\<And>G nP::('v \<Rightarrow> 'a). wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP"
    shows "minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) fs keeps G =
       TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) fs keeps (list_graph_to_graph G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) fs keeps G = TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) fs keeps (list_graph_to_graph G)
[PROOF STEP]
apply(subst minimalize_offending_overapprox_boundnP)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) fs keeps G = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs keeps (list_graph_to_graph G) nP
[PROOF STEP]
using valid spec_impl
[PROOF STATE]
proof (prove)
using this:
wf_list_graph G
wf_list_graph ?G \<Longrightarrow> sinvar_spec (list_graph_to_graph ?G) ?nP = sinvar_impl ?G ?nP

goal (1 subgoal):
 1. TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) fs keeps G = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs keeps (list_graph_to_graph G) nP
[PROOF STEP]
apply(induction fs arbitrary: keeps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>keeps. \<lbrakk>wf_list_graph G; \<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP\<rbrakk> \<Longrightarrow> TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) [] keeps G = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec [] keeps (list_graph_to_graph G) nP
 2. \<And>a fs keeps. \<lbrakk>\<And>keeps. \<lbrakk>wf_list_graph G; \<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP\<rbrakk> \<Longrightarrow> TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) fs keeps G = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs keeps (list_graph_to_graph G) nP; wf_list_graph G; \<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP\<rbrakk> \<Longrightarrow> TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) (a # fs) keeps G = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec (a # fs) keeps (list_graph_to_graph G) nP
[PROOF STEP]
apply(simp add: SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox.simps; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a fs keeps. \<lbrakk>\<And>keeps. \<lbrakk>wf_list_graph G; \<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP\<rbrakk> \<Longrightarrow> TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) fs keeps G = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs keeps (list_graph_to_graph G) nP; wf_list_graph G; \<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP\<rbrakk> \<Longrightarrow> TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) (a # fs) keeps G = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec (a # fs) keeps (list_graph_to_graph G) nP
[PROOF STEP]
apply(simp add: SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a fs keeps. \<lbrakk>\<And>keeps. TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. sinvar_impl G nP) fs keeps G = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs keeps (list_graph_to_graph G) nP; wf_list_graph G; \<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = sinvar_impl G nP\<rbrakk> \<Longrightarrow> (sinvar_impl (FiniteListGraph.delete_edges G (fs @ keeps)) nP \<longrightarrow> \<not> sinvar_spec (delete_edges_list (list_graph_to_graph G) (fs @ keeps)) nP \<longrightarrow> SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs keeps (list_graph_to_graph G) nP = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs (a # keeps) (list_graph_to_graph G) nP) \<and> (\<not> sinvar_impl (FiniteListGraph.delete_edges G (fs @ keeps)) nP \<longrightarrow> sinvar_spec (delete_edges_list (list_graph_to_graph G) (fs @ keeps)) nP \<longrightarrow> SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs (a # keeps) (list_graph_to_graph G) nP = SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec fs keeps (list_graph_to_graph G) nP)
[PROOF STEP]
apply (metis FiniteListGraph.delete_edges_wf delete_edges_list_set list_graph_correct(5))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma minimalize_offending_overapprox_gives_some_offending_flow:
    assumes wf: "wf_list_graph G"
        and NetModelLib: "TopoS_modelLibrary m sinvar_spec"
        and violation: "\<not> (nm_sinvar m) G nP"
    shows "set (minimalize_offending_overapprox (\<lambda>G. (nm_sinvar m) G nP) (edgesL G) [] G) \<in>
            SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_list_graph G
[PROOF STEP]
have wfG: "wf_graph (list_graph_to_graph G)"
[PROOF STATE]
proof (prove)
using this:
wf_list_graph G

goal (1 subgoal):
 1. wf_graph (list_graph_to_graph G)
[PROOF STEP]
by (simp add: wf_list_graph_def wf_list_graph_iff_wf_graph)
[PROOF STATE]
proof (state)
this:
wf_graph (list_graph_to_graph G)

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_list_graph G
[PROOF STEP]
have dist_edges: "distinct (edgesL G)"
[PROOF STATE]
proof (prove)
using this:
wf_list_graph G

goal (1 subgoal):
 1. distinct (edgesL G)
[PROOF STEP]
by (simp add: wf_list_graph_def)
[PROOF STATE]
proof (state)
this:
distinct (edgesL G)

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
let ?spec_algo="TopoS_withOffendingFlows.minimalize_offending_overapprox
                          (\<lambda>G. sinvar_spec G nP) (edgesL G) [] (list_graph_to_graph G)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
note spec=TopoS_List_Impl.spec[OF TopoS_modelLibrary.impl_spec[OF NetModelLib]]
[PROOF STATE]
proof (state)
this:
SecurityInvariant sinvar_spec (nm_default m) (nm_receiver_violation m)

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from spec
[PROOF STATE]
proof (chain)
picking this:
SecurityInvariant sinvar_spec (nm_default m) (nm_receiver_violation m)
[PROOF STEP]
have spec_prelim: "SecurityInvariant_preliminaries sinvar_spec"
[PROOF STATE]
proof (prove)
using this:
SecurityInvariant sinvar_spec (nm_default m) (nm_receiver_violation m)

goal (1 subgoal):
 1. SecurityInvariant_preliminaries sinvar_spec
[PROOF STEP]
by(simp add: SecurityInvariant_def)
[PROOF STATE]
proof (state)
this:
SecurityInvariant_preliminaries sinvar_spec

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from spec_prelim SecurityInvariant_preliminaries.sinvar_monoI
[PROOF STATE]
proof (chain)
picking this:
SecurityInvariant_preliminaries sinvar_spec
SecurityInvariant_preliminaries ?sinvar \<Longrightarrow> SecurityInvariant_withOffendingFlows.sinvar_mono ?sinvar
[PROOF STEP]
have mono:
        "SecurityInvariant_withOffendingFlows.sinvar_mono sinvar_spec"
[PROOF STATE]
proof (prove)
using this:
SecurityInvariant_preliminaries sinvar_spec
SecurityInvariant_preliminaries ?sinvar \<Longrightarrow> SecurityInvariant_withOffendingFlows.sinvar_mono ?sinvar

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

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from spec_prelim
[PROOF STATE]
proof (chain)
picking this:
SecurityInvariant_preliminaries sinvar_spec
[PROOF STEP]
have empty_edges: "sinvar_spec \<lparr>nodes = set (nodesL G), edges = {}\<rparr> nP"
[PROOF STATE]
proof (prove)
using this:
SecurityInvariant_preliminaries sinvar_spec

goal (1 subgoal):
 1. sinvar_spec \<lparr>nodes = set (nodesL G), edges = {}\<rparr> nP
[PROOF STEP]
using SecurityInvariant_preliminaries.defined_offending
        SecurityInvariant_withOffendingFlows.sinvar_mono_imp_sinvar_mono
        SecurityInvariant_withOffendingFlows.valid_empty_edges_iff_exists_offending_flows
        mono empty_subsetI graph.simps(1)
        list_graph_to_graph_def local.wf wf_list_graph_def wf_list_graph_iff_wf_graph
[PROOF STATE]
proof (prove)
using this:
SecurityInvariant_preliminaries sinvar_spec
\<lbrakk>SecurityInvariant_preliminaries ?sinvar; wf_graph ?G; \<not> ?sinvar ?G ?nP\<rbrakk> \<Longrightarrow> SecurityInvariant_withOffendingFlows.set_offending_flows ?sinvar ?G ?nP \<noteq> {}
\<lbrakk>SecurityInvariant_withOffendingFlows.sinvar_mono ?sinvar; wf_graph \<lparr>nodes = ?N, edges = ?E\<rparr>; ?E' \<subseteq> ?E; ?sinvar \<lparr>nodes = ?N, edges = ?E\<rparr> ?nP\<rbrakk> \<Longrightarrow> ?sinvar \<lparr>nodes = ?N, edges = ?E'\<rparr> ?nP
\<lbrakk>SecurityInvariant_withOffendingFlows.sinvar_mono ?sinvar; wf_graph ?G; \<not> ?sinvar ?G ?nP\<rbrakk> \<Longrightarrow> ?sinvar \<lparr>nodes = nodes ?G, edges = {}\<rparr> ?nP = (SecurityInvariant_withOffendingFlows.set_offending_flows ?sinvar ?G ?nP \<noteq> {})
SecurityInvariant_withOffendingFlows.sinvar_mono sinvar_spec
{} \<subseteq> ?A
nodes \<lparr>nodes = ?nodes, edges = ?edges, \<dots> = ?more\<rparr> = ?nodes
list_graph_to_graph ?G = \<lparr>nodes = set (nodesL ?G), edges = set (edgesL ?G)\<rparr>
wf_list_graph G
wf_list_graph ?G = (distinct (nodesL ?G) \<and> distinct (edgesL ?G) \<and> wf_list_graph_axioms ?G)
wf_graph (list_graph_to_graph ?G) = wf_list_graph_axioms ?G

goal (1 subgoal):
 1. sinvar_spec \<lparr>nodes = set (nodesL G), edges = {}\<rparr> nP
[PROOF STEP]
by (metis)
[PROOF STATE]
proof (state)
this:
sinvar_spec \<lparr>nodes = set (nodesL G), edges = {}\<rparr> nP

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
(*TODO: tune*)
[PROOF STATE]
proof (state)
this:
sinvar_spec \<lparr>nodes = set (nodesL G), edges = {}\<rparr> nP

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
have spec_impl: "wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = (nm_sinvar m) G nP" for G nP
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = nm_sinvar m G nP
[PROOF STEP]
using NetModelLib TopoS_List_Impl.sinvar_spec_impl TopoS_modelLibrary.impl_spec
[PROOF STATE]
proof (prove)
using this:
TopoS_modelLibrary m sinvar_spec
\<lbrakk>TopoS_List_Impl ?default_node_properties ?sinvar_spec ?sinvar_impl ?receiver_violation ?offending_flows_impl ?node_props_impl ?eval_impl; wf_list_graph ?G\<rbrakk> \<Longrightarrow> ?sinvar_spec (list_graph_to_graph ?G) ?nP = ?sinvar_impl ?G ?nP
TopoS_modelLibrary ?m ?sinvar_spec \<Longrightarrow> TopoS_List_Impl (nm_default ?m) ?sinvar_spec (nm_sinvar ?m) (nm_receiver_violation ?m) (nm_offending_flows ?m) (nm_node_props ?m) (nm_eval ?m)

goal (1 subgoal):
 1. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = nm_sinvar m G nP
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
wf_list_graph ?G \<Longrightarrow> sinvar_spec (list_graph_to_graph ?G) ?nP = nm_sinvar m ?G ?nP

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from minimalize_offending_overapprox_spec_impl[OF wf] spec_impl
[PROOF STATE]
proof (chain)
picking this:
(\<And>G nP. wf_list_graph G \<Longrightarrow> ?sinvar_spec (list_graph_to_graph G) nP = ?sinvar_impl G nP) \<Longrightarrow> TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. ?sinvar_impl G ?nP) ?fs ?keeps G = TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. ?sinvar_spec G ?nP) ?fs ?keeps (list_graph_to_graph G)
wf_list_graph ?G \<Longrightarrow> sinvar_spec (list_graph_to_graph ?G) ?nP = nm_sinvar m ?G ?nP
[PROOF STEP]
have alog_spec:
        "minimalize_offending_overapprox (\<lambda>G. (nm_sinvar m) G nP) fs keeps G =
         TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) fs keeps (list_graph_to_graph G)"
         for fs keeps
[PROOF STATE]
proof (prove)
using this:
(\<And>G nP. wf_list_graph G \<Longrightarrow> ?sinvar_spec (list_graph_to_graph G) nP = ?sinvar_impl G nP) \<Longrightarrow> TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. ?sinvar_impl G ?nP) ?fs ?keeps G = TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. ?sinvar_spec G ?nP) ?fs ?keeps (list_graph_to_graph G)
wf_list_graph ?G \<Longrightarrow> sinvar_spec (list_graph_to_graph ?G) ?nP = nm_sinvar m ?G ?nP

goal (1 subgoal):
 1. TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) fs keeps G = TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) fs keeps (list_graph_to_graph G)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) ?fs ?keeps G = TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) ?fs ?keeps (list_graph_to_graph G)

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
(*TODO: tune*)
[PROOF STATE]
proof (state)
this:
TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) ?fs ?keeps G = TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) ?fs ?keeps (list_graph_to_graph G)

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from spec_impl violation
[PROOF STATE]
proof (chain)
picking this:
wf_list_graph ?G \<Longrightarrow> sinvar_spec (list_graph_to_graph ?G) ?nP = nm_sinvar m ?G ?nP
\<not> nm_sinvar m G nP
[PROOF STEP]
have
        "SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP"
[PROOF STATE]
proof (prove)
using this:
wf_list_graph ?G \<Longrightarrow> sinvar_spec (list_graph_to_graph ?G) ?nP = nm_sinvar m ?G ?nP
\<not> nm_sinvar m G nP

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP
[PROOF STEP]
apply(simp add: SecurityInvariant_withOffendingFlows.is_offending_flows_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = nm_sinvar m G nP; \<not> nm_sinvar m G nP\<rbrakk> \<Longrightarrow> \<not> sinvar_spec (list_graph_to_graph G) nP \<and> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set (edgesL G))) nP
[PROOF STEP]
apply(intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = nm_sinvar m G nP; \<not> nm_sinvar m G nP\<rbrakk> \<Longrightarrow> \<not> sinvar_spec (list_graph_to_graph G) nP
 2. \<lbrakk>\<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = nm_sinvar m G nP; \<not> nm_sinvar m G nP\<rbrakk> \<Longrightarrow> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set (edgesL G))) nP
[PROOF STEP]
apply (simp add: local.wf; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec (list_graph_to_graph G) nP = nm_sinvar m G nP; \<not> nm_sinvar m G nP\<rbrakk> \<Longrightarrow> sinvar_spec (FiniteGraph.delete_edges (list_graph_to_graph G) (set (edgesL G))) nP
[PROOF STEP]
apply(simp add: FiniteGraph.delete_edges_simp2 list_graph_to_graph_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>G nP. wf_list_graph G \<Longrightarrow> sinvar_spec \<lparr>nodes = set (nodesL G), edges = set (edgesL G)\<rparr> nP = nm_sinvar m G nP; \<not> nm_sinvar m G nP\<rbrakk> \<Longrightarrow> sinvar_spec \<lparr>nodes = set (nodesL G), edges = {}\<rparr> nP
[PROOF STEP]
apply(simp add: empty_edges)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
hence goal: "SecurityInvariant_withOffendingFlows.is_offending_flows_min_set sinvar_spec
        (set ?spec_algo) (list_graph_to_graph G) nP"
[PROOF STATE]
proof (prove)
using this:
SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP

goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.is_offending_flows_min_set sinvar_spec (set (TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) (edgesL G) [] (list_graph_to_graph G))) (list_graph_to_graph G) nP
[PROOF STEP]
apply(subst minimalize_offending_overapprox_boundnP)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP \<Longrightarrow> SecurityInvariant_withOffendingFlows.is_offending_flows_min_set sinvar_spec (set (SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec (edgesL G) [] (list_graph_to_graph G) nP)) (list_graph_to_graph G) nP
[PROOF STEP]
(*we do this subst pretty often. is this the right abstraction here?*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP \<Longrightarrow> SecurityInvariant_withOffendingFlows.is_offending_flows_min_set sinvar_spec (set (SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec (edgesL G) [] (list_graph_to_graph G) nP)) (list_graph_to_graph G) nP
[PROOF STEP]
apply(rule SecurityInvariant_withOffendingFlows.is_offending_flows_min_set_minimalize_offending_overapprox[OF
              mono wfG _ _ dist_edges])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP \<Longrightarrow> SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP
 2. SecurityInvariant_withOffendingFlows.is_offending_flows sinvar_spec (set (edgesL G)) (list_graph_to_graph G) nP \<Longrightarrow> set (edgesL G) \<subseteq> edges (list_graph_to_graph G)
[PROOF STEP]
apply(simp add: list_graph_to_graph_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
SecurityInvariant_withOffendingFlows.is_offending_flows_min_set sinvar_spec (set (TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) (edgesL G) [] (list_graph_to_graph G))) (list_graph_to_graph G) nP

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox_subseteq_input[of
        "sinvar_spec" "(edgesL G)" "[]"]
[PROOF STATE]
proof (chain)
picking this:
set (SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec (edgesL G) [] ?G ?nP) \<subseteq> set (edgesL G) \<union> set []
[PROOF STEP]
have subset_edges:
        "set ?spec_algo \<subseteq> edges (list_graph_to_graph G)"
[PROOF STATE]
proof (prove)
using this:
set (SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec (edgesL G) [] ?G ?nP) \<subseteq> set (edgesL G) \<union> set []

goal (1 subgoal):
 1. set (TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) (edgesL G) [] (list_graph_to_graph G)) \<subseteq> edges (list_graph_to_graph G)
[PROOF STEP]
apply(subst minimalize_offending_overapprox_boundnP)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ga nP. set (SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec (edgesL G) [] Ga nP) \<subseteq> set (edgesL G) \<union> set []) \<Longrightarrow> set (SecurityInvariant_withOffendingFlows.minimalize_offending_overapprox sinvar_spec (edgesL G) [] (list_graph_to_graph G) nP) \<subseteq> edges (list_graph_to_graph G)
[PROOF STEP]
by(simp add: list_graph_to_graph_def)
[PROOF STATE]
proof (state)
this:
set (TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) (edgesL G) [] (list_graph_to_graph G)) \<subseteq> edges (list_graph_to_graph G)

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
from goal
[PROOF STATE]
proof (chain)
picking this:
SecurityInvariant_withOffendingFlows.is_offending_flows_min_set sinvar_spec (set (TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) (edgesL G) [] (list_graph_to_graph G))) (list_graph_to_graph G) nP
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
SecurityInvariant_withOffendingFlows.is_offending_flows_min_set sinvar_spec (set (TopoS_withOffendingFlows.minimalize_offending_overapprox (\<lambda>G. sinvar_spec G nP) (edgesL G) [] (list_graph_to_graph G))) (list_graph_to_graph G) nP

goal (1 subgoal):
 1. set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP
[PROOF STEP]
by(simp add: SecurityInvariant_withOffendingFlows.set_offending_flows_def alog_spec subset_edges)
[PROOF STATE]
proof (state)
this:
set (TopoS_Interface_impl.minimalize_offending_overapprox (\<lambda>G. nm_sinvar m G nP) (edgesL G) [] G) \<in> SecurityInvariant_withOffendingFlows.set_offending_flows sinvar_spec (list_graph_to_graph G) nP

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fresh_imp_notin_env: "atom name \<sharp> e \<Longrightarrow> name \<notin> set e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom name \<sharp> e \<Longrightarrow> name \<notin> set e
[PROOF STEP]
by (metis List.finite_set fresh_finite_set_at_base fresh_set)


[STATEMENT]
lemma lookup_notin: "x \<notin> set e \<Longrightarrow> lookup e n x = DBVar x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set e \<Longrightarrow> lookup e n x = DBVar x
[PROOF STEP]
by (induct e arbitrary: n) auto


[STATEMENT]
lemma lookup_in:
  "x \<in> set e \<Longrightarrow> \<exists>k. lookup e n x = DBInd k \<and> n \<le> k \<and> k < n + length e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set e \<Longrightarrow> \<exists>k. lookup e n x = DBInd k \<and> n \<le> k \<and> k < n + length e
[PROOF STEP]
apply (induct e arbitrary: n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. x \<in> set [] \<Longrightarrow> \<exists>k. lookup [] n x = DBInd k \<and> n \<le> k \<and> k < n + length []
 2. \<And>a e n. \<lbrakk>\<And>n. x \<in> set e \<Longrightarrow> \<exists>k. lookup e n x = DBInd k \<and> n \<le> k \<and> k < n + length e; x \<in> set (a # e)\<rbrakk> \<Longrightarrow> \<exists>k. lookup (a # e) n x = DBInd k \<and> n \<le> k \<and> k < n + length (a # e)
[PROOF STEP]
apply (auto intro: Suc_leD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a e n. \<lbrakk>\<And>n. \<exists>k. lookup e n x = DBInd k \<and> n \<le> k \<and> k < n + length e; x \<noteq> a; x \<in> set e\<rbrakk> \<Longrightarrow> \<exists>k. lookup e (Suc n) x = DBInd k \<and> n \<le> k \<and> k < Suc (n + length e)
[PROOF STEP]
apply (metis Suc_leD add_Suc_right add_Suc_shift)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lookup_fresh: "x \<sharp> lookup e n y \<longleftrightarrow> y \<in> set e \<or> x \<noteq> atom y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> lookup e n y = (y \<in> set e \<or> x \<noteq> atom y)
[PROOF STEP]
by (induct arbitrary: n rule: lookup.induct) (auto simp: pure_fresh fresh_at_base)


[STATEMENT]
lemma lookup_eqvt[eqvt]: "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> lookup xs n x = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)
[PROOF STEP]
by (induct xs arbitrary: n) (simp_all add: permute_pure)


[STATEMENT]
lemma lookup_inject [iff]: "(lookup e n x = lookup e n y) \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lookup e n x = lookup e n y) = (x = y)
[PROOF STEP]
apply (induct e n x arbitrary: y rule: lookup.induct, force, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ys n x ya. (\<And>ya. x \<noteq> y \<Longrightarrow> (lookup ys (Suc n) x = lookup ys (Suc n) ya) = (x = ya)) \<Longrightarrow> (x = y \<longrightarrow> ya \<noteq> y \<longrightarrow> DBInd n \<noteq> lookup ys (Suc n) ya) \<and> (x \<noteq> y \<longrightarrow> ya = y \<longrightarrow> lookup ys (Suc n) x \<noteq> DBInd n)
[PROOF STEP]
by (metis Suc_n_not_le_n dbtm.distinct(7) dbtm.eq_iff(3) lookup_in lookup_notin)


[STATEMENT]
lemma fresh_trans_tm_iff [simp]: "i \<sharp> trans_tm e t \<longleftrightarrow> i \<sharp> t \<or> i \<in> atom ` set e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<sharp> trans_tm e t = (i \<sharp> t \<or> i \<in> atom ` set e)
[PROOF STEP]
by (induct t rule: tm.induct, auto simp: lookup_fresh fresh_at_base)


[STATEMENT]
lemma trans_tm_forget: "atom i \<sharp> t \<Longrightarrow> trans_tm [i] t = trans_tm [] t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> t \<Longrightarrow> trans_tm [i] t = trans_tm [] t
[PROOF STEP]
by (induct t rule: tm.induct, auto simp: fresh_Pair)