[STATEMENT]
lemma subst_fml:
  fixes I::"('sf, 'sc, 'sz) interp" and \<nu>::"'sz state"
  assumes good_interp:"is_interp I"
  assumes Fadmit:"Fadmit \<sigma> \<phi>"
  assumes fsafe:"fsafe \<phi>"
  assumes ssafe:"ssafe \<sigma>"
  shows "(\<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)) = (\<nu> \<in> fml_sem (adjoint I \<sigma> \<nu>) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>)
[PROOF STEP]
using subst_fml_hp[OF good_interp] Fadmit fsafe ssafe
[PROOF STATE]
proof (prove)
using this:
(Padmit ?\<sigma> ?\<alpha> \<longrightarrow> hpsafe ?\<alpha> \<longrightarrow> ssafe ?\<sigma> \<longrightarrow> (\<forall>\<nu> \<omega>. ((\<nu>, \<omega>) \<in> prog_sem I (Psubst ?\<alpha> ?\<sigma>)) = ((\<nu>, \<omega>) \<in> prog_sem (local.adjoint I ?\<sigma> \<nu>) ?\<alpha>))) \<and> (Fadmit ?\<sigma> ?\<phi> \<longrightarrow> fsafe ?\<phi> \<longrightarrow> ssafe ?\<sigma> \<longrightarrow> (\<forall>\<nu>. (\<nu> \<in> fml_sem I (Fsubst ?\<phi> ?\<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I ?\<sigma> \<nu>) ?\<phi>)))
Fadmit \<sigma> \<phi>
fsafe \<phi>
ssafe \<sigma>

goal (1 subgoal):
 1. (\<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>)
[PROOF STEP]
by blast


[STATEMENT]
lemma subst_fml_valid:
  fixes I::"('sf, 'sc, 'sz) interp" and \<nu>::"'sz state"
  assumes Fadmit:"Fadmit \<sigma> \<phi>"
  assumes fsafe:"fsafe \<phi>"
  assumes ssafe:"ssafe \<sigma>"
  assumes valid:"valid \<phi>"
  shows "valid (Fsubst \<phi> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid (Fsubst \<phi> \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. valid (Fsubst \<phi> \<sigma>)
[PROOF STEP]
have sub_sem:"\<And>I \<nu>. is_interp I \<Longrightarrow> \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I \<nu>. is_interp I \<Longrightarrow> \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I \<nu>. is_interp I \<Longrightarrow> \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
fix I::"('sf,'sc,'sz) interp" and \<nu>::"'sz state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I \<nu>. is_interp I \<Longrightarrow> \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
assume good_interp:"is_interp I"
[PROOF STATE]
proof (state)
this:
is_interp I

goal (1 subgoal):
 1. \<And>I \<nu>. is_interp I \<Longrightarrow> \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
have good_adj:"is_interp (adjoint I \<sigma> \<nu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_interp (local.adjoint I \<sigma> \<nu>)
[PROOF STEP]
apply(rule adjoint_safe[OF good_interp])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'
[PROOF STEP]
using ssafe
[PROOF STATE]
proof (prove)
using this:
ssafe \<sigma>

goal (1 subgoal):
 1. \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'
[PROOF STEP]
unfolding ssafe_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i f'. SFunctions \<sigma> i = Some f' \<longrightarrow> dfree f') \<and> (\<forall>f f'. SPredicates \<sigma> f = Some f' \<longrightarrow> fsafe f') \<and> (\<forall>f f'. SPrograms \<sigma> f = Some f' \<longrightarrow> hpsafe f') \<and> (\<forall>f f'. SODEs \<sigma> f = Some f' \<longrightarrow> osafe f') \<and> (\<forall>C C'. SContexts \<sigma> C = Some C' \<longrightarrow> fsafe C')

goal (1 subgoal):
 1. \<And>i f'. SFunctions \<sigma> i = Some f' \<Longrightarrow> dfree f'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_interp (local.adjoint I \<sigma> \<nu>)

goal (1 subgoal):
 1. \<And>I \<nu>. is_interp I \<Longrightarrow> \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
have \<phi>sem:"\<nu> \<in> fml_sem (adjoint I \<sigma> \<nu>) \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
valid \<phi>

goal (1 subgoal):
 1. \<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
using good_adj
[PROOF STATE]
proof (prove)
using this:
valid \<phi>
is_interp (local.adjoint I \<sigma> \<nu>)

goal (1 subgoal):
 1. \<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
using this:
\<forall>I \<nu>. is_interp I \<longrightarrow> \<nu> \<in> fml_sem I \<phi>
is_interp (local.adjoint I \<sigma> \<nu>)

goal (1 subgoal):
 1. \<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>

goal (1 subgoal):
 1. \<And>I \<nu>. is_interp I \<Longrightarrow> \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
show "?thesis I \<nu>"
[PROOF STATE]
proof (prove)
using this:
\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>

goal (1 subgoal):
 1. \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
using subst_fml[OF good_interp Fadmit fsafe ssafe]
[PROOF STATE]
proof (prove)
using this:
\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) \<phi>
(?\<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)) = (?\<nu> \<in> fml_sem (local.adjoint I \<sigma> ?\<nu>) \<phi>)

goal (1 subgoal):
 1. \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_interp ?I7 \<Longrightarrow> ?\<nu>7 \<in> fml_sem ?I7 (Fsubst \<phi> \<sigma>)

goal (1 subgoal):
 1. valid (Fsubst \<phi> \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_interp ?I7 \<Longrightarrow> ?\<nu>7 \<in> fml_sem ?I7 (Fsubst \<phi> \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_interp ?I7 \<Longrightarrow> ?\<nu>7 \<in> fml_sem ?I7 (Fsubst \<phi> \<sigma>)

goal (1 subgoal):
 1. valid (Fsubst \<phi> \<sigma>)
[PROOF STEP]
unfolding valid_def
[PROOF STATE]
proof (prove)
using this:
is_interp ?I7 \<Longrightarrow> ?\<nu>7 \<in> fml_sem ?I7 (Fsubst \<phi> \<sigma>)

goal (1 subgoal):
 1. \<forall>I \<nu>. is_interp I \<longrightarrow> \<nu> \<in> fml_sem I (Fsubst \<phi> \<sigma>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
valid (Fsubst \<phi> \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_sequent:
  fixes I::"('sf, 'sc, 'sz) interp" and \<nu>::"'sz state"
  assumes good_interp:"is_interp I"
  assumes Sadmit:"Sadmit \<sigma> (\<Gamma>,\<Delta>)"
  assumes Ssafe:"Ssafe (\<Gamma>,\<Delta>)"
  assumes ssafe:"ssafe \<sigma>"
  shows "(\<nu> \<in> seq_sem I (Ssubst (\<Gamma>,\<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (adjoint I \<sigma> \<nu>) (\<Gamma>,\<Delta>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
let ?f = "(seq2fml (\<Gamma>, \<Delta>))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have subst_eqG:"Fsubst (foldr (&&) \<Gamma> TT) \<sigma> = foldr (&&) (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>) TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fsubst (foldr (&&) \<Gamma> TT) \<sigma> = foldr (&&) (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>) TT
[PROOF STEP]
by(induction \<Gamma>, auto simp add: TT_def)
[PROOF STATE]
proof (state)
this:
Fsubst (foldr (&&) \<Gamma> TT) \<sigma> = foldr (&&) (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>) TT

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have subst_eqD:"Fsubst (foldr (||) \<Delta> FF) \<sigma> = foldr (||) (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>) FF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fsubst (foldr (||) \<Delta> FF) \<sigma> = foldr (||) (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>) FF
[PROOF STEP]
by(induction \<Delta>, auto simp add: FF_def Or_def)
[PROOF STATE]
proof (state)
this:
Fsubst (foldr (||) \<Delta> FF) \<sigma> = foldr (||) (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>) FF

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have subst_eq:"Fsubst ?f \<sigma> = (seq2fml (Ssubst (\<Gamma>, \<Delta>) \<sigma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma> = seq2fml (Ssubst (\<Gamma>, \<Delta>) \<sigma>)
[PROOF STEP]
using subst_eqG subst_eqD
[PROOF STATE]
proof (prove)
using this:
Fsubst (foldr (&&) \<Gamma> TT) \<sigma> = foldr (&&) (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>) TT
Fsubst (foldr (||) \<Delta> FF) \<sigma> = foldr (||) (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>) FF

goal (1 subgoal):
 1. Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma> = seq2fml (Ssubst (\<Gamma>, \<Delta>) \<sigma>)
[PROOF STEP]
by (auto simp add: Implies_def Or_def)
[PROOF STATE]
proof (state)
this:
Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma> = seq2fml (Ssubst (\<Gamma>, \<Delta>) \<sigma>)

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have fsafeG:"fsafe (foldr (&&) \<Gamma> TT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fsafe (foldr (&&) \<Gamma> TT)
[PROOF STEP]
using Ssafe
[PROOF STATE]
proof (prove)
using this:
Ssafe (\<Gamma>, \<Delta>)

goal (1 subgoal):
 1. fsafe (foldr (&&) \<Gamma> TT)
[PROOF STEP]
apply(induction \<Gamma>, auto simp add: Ssafe_def TT_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a \<Gamma>'. \<lbrakk>\<forall>i<length \<Gamma>'. fsafe (\<Gamma>' ! i) \<Longrightarrow> fsafe (foldr (&&) \<Gamma>' (Geq (Const 0) (Const 0))); \<forall>i<length \<Gamma>. fsafe (\<Gamma> ! i); \<forall>i<Suc (length \<Gamma>'). fsafe ((a # \<Gamma>') ! i); \<forall>i<length \<Delta>. fsafe (\<Delta> ! i)\<rbrakk> \<Longrightarrow> fsafe (foldr (&&) \<Gamma>' (Geq (Const 0) (Const 0)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
fsafe (foldr (&&) \<Gamma> TT)

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have fsafeD:"fsafe (foldr (||) \<Delta> FF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fsafe (foldr (||) \<Delta> FF)
[PROOF STEP]
using Ssafe Or_def
[PROOF STATE]
proof (prove)
using this:
Ssafe (\<Gamma>, \<Delta>)
(?P || ?Q) = ! (! ?P && ! ?Q)

goal (1 subgoal):
 1. fsafe (foldr (||) \<Delta> FF)
[PROOF STEP]
apply(induction \<Delta>, auto simp add: Ssafe_def FF_def Or_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a \<Delta>'. \<lbrakk>\<forall>i<length \<Delta>'. fsafe (\<Delta>' ! i) \<Longrightarrow> fsafe (foldr (||) \<Delta>' (Geq (Const 0) (Const 1))); \<forall>i<length \<Delta>. fsafe (\<Delta> ! i); \<forall>i<length \<Gamma>. fsafe (\<Gamma> ! i); \<forall>i<Suc (length \<Delta>'). fsafe ((a # \<Delta>') ! i)\<rbrakk> \<Longrightarrow> fsafe (foldr (||) \<Delta>' (Geq (Const 0) (Const 1)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
fsafe (foldr (||) \<Delta> FF)

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have fsafe:"fsafe ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fsafe (seq2fml (\<Gamma>, \<Delta>))
[PROOF STEP]
using fsafeD fsafeG
[PROOF STATE]
proof (prove)
using this:
fsafe (foldr (||) \<Delta> FF)
fsafe (foldr (&&) \<Gamma> TT)

goal (1 subgoal):
 1. fsafe (seq2fml (\<Gamma>, \<Delta>))
[PROOF STEP]
by (auto simp add: Implies_def Or_def)
[PROOF STATE]
proof (state)
this:
fsafe (seq2fml (\<Gamma>, \<Delta>))

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have FadmitG:"Fadmit \<sigma> (foldr (&&) \<Gamma> TT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fadmit \<sigma> (foldr (&&) \<Gamma> TT)
[PROOF STEP]
using Sadmit Or_def
[PROOF STATE]
proof (prove)
using this:
Sadmit \<sigma> (\<Gamma>, \<Delta>)
(?P || ?Q) = ! (! ?P && ! ?Q)

goal (1 subgoal):
 1. Fadmit \<sigma> (foldr (&&) \<Gamma> TT)
[PROOF STEP]
apply(induction \<Gamma>, auto simp add: Sadmit_def TT_def Or_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a \<Gamma>'. \<lbrakk>\<forall>i<length \<Gamma>'. Fadmit \<sigma> (\<Gamma>' ! i) \<Longrightarrow> Fadmit \<sigma> (foldr (&&) \<Gamma>' (Geq (Const 0) (Const 0))); \<forall>i<length \<Gamma>. Fadmit \<sigma> (\<Gamma> ! i); \<forall>i<Suc (length \<Gamma>'). Fadmit \<sigma> ((a # \<Gamma>') ! i); \<forall>i<length \<Delta>. Fadmit \<sigma> (\<Delta> ! i)\<rbrakk> \<Longrightarrow> Fadmit \<sigma> (foldr (&&) \<Gamma>' (Geq (Const 0) (Const 0)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Fadmit \<sigma> (foldr (&&) \<Gamma> TT)

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have FadmitD:"Fadmit \<sigma> (foldr (||) \<Delta> FF)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fadmit \<sigma> (foldr (||) \<Delta> FF)
[PROOF STEP]
using Sadmit Or_def
[PROOF STATE]
proof (prove)
using this:
Sadmit \<sigma> (\<Gamma>, \<Delta>)
(?P || ?Q) = ! (! ?P && ! ?Q)

goal (1 subgoal):
 1. Fadmit \<sigma> (foldr (||) \<Delta> FF)
[PROOF STEP]
apply(induction \<Delta>, auto simp add: Sadmit_def FF_def Or_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a \<Delta>'. \<lbrakk>\<forall>i<length \<Delta>'. Fadmit \<sigma> (\<Delta>' ! i) \<Longrightarrow> Fadmit \<sigma> (foldr (||) \<Delta>' (Geq (Const 0) (Const 1))); \<forall>i<length \<Delta>. Fadmit \<sigma> (\<Delta> ! i); \<forall>i<length \<Gamma>. Fadmit \<sigma> (\<Gamma> ! i); \<forall>i<Suc (length \<Delta>'). Fadmit \<sigma> ((a # \<Delta>') ! i)\<rbrakk> \<Longrightarrow> Fadmit \<sigma> (foldr (||) \<Delta>' (Geq (Const 0) (Const 1)))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Fadmit \<sigma> (foldr (||) \<Delta> FF)

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have Fadmit:"Fadmit \<sigma> ?f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fadmit \<sigma> (seq2fml (\<Gamma>, \<Delta>))
[PROOF STEP]
using FadmitG FadmitD
[PROOF STATE]
proof (prove)
using this:
Fadmit \<sigma> (foldr (&&) \<Gamma> TT)
Fadmit \<sigma> (foldr (||) \<Delta> FF)

goal (1 subgoal):
 1. Fadmit \<sigma> (seq2fml (\<Gamma>, \<Delta>))
[PROOF STEP]
unfolding Implies_def
[PROOF STATE]
proof (prove)
using this:
Fadmit \<sigma> (foldr (&&) \<Gamma> TT)
Fadmit \<sigma> (foldr (||) \<Delta> FF)

goal (1 subgoal):
 1. Fadmit \<sigma> (seq2fml (\<Gamma>, \<Delta>))
[PROOF STEP]
by (simp add: Implies_def Or_def)
[PROOF STATE]
proof (state)
this:
Fadmit \<sigma> (seq2fml (\<Gamma>, \<Delta>))

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
have "(\<nu> \<in> fml_sem I (Fsubst ?f \<sigma>))
       =(\<nu> \<in> fml_sem (adjoint I \<sigma> \<nu>) (seq2fml (\<Gamma>, \<Delta>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> \<in> fml_sem I (Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) (seq2fml (\<Gamma>, \<Delta>)))
[PROOF STEP]
using subst_fml[OF good_interp Fadmit fsafe ssafe]
[PROOF STATE]
proof (prove)
using this:
(?\<nu> \<in> fml_sem I (Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma>)) = (?\<nu> \<in> fml_sem (local.adjoint I \<sigma> ?\<nu>) (seq2fml (\<Gamma>, \<Delta>)))

goal (1 subgoal):
 1. (\<nu> \<in> fml_sem I (Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) (seq2fml (\<Gamma>, \<Delta>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<nu> \<in> fml_sem I (Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) (seq2fml (\<Gamma>, \<Delta>)))

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<nu> \<in> fml_sem I (Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) (seq2fml (\<Gamma>, \<Delta>)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<nu> \<in> fml_sem I (Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) (seq2fml (\<Gamma>, \<Delta>)))

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
using subst_eq
[PROOF STATE]
proof (prove)
using this:
(\<nu> \<in> fml_sem I (Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma>)) = (\<nu> \<in> fml_sem (local.adjoint I \<sigma> \<nu>) (seq2fml (\<Gamma>, \<Delta>)))
Fsubst (seq2fml (\<Gamma>, \<Delta>)) \<sigma> = seq2fml (Ssubst (\<Gamma>, \<Delta>) \<sigma>)

goal (1 subgoal):
 1. (\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<nu> \<in> seq_sem I (Ssubst (\<Gamma>, \<Delta>) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>, \<Delta>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem subst_rule:
  assumes sound:"sound R"
  assumes Radmit:"Radmit \<sigma> R"
  assumes FVS:"FVS \<sigma> = {}"
  assumes Rsafe:"Rsafe R"
  assumes ssafe:"ssafe \<sigma>"
  shows "sound (Rsubst R \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
obtain SG and C where Rdef:"R = (SG,C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>SG C. R = (SG, C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases R, auto)
[PROOF STATE]
proof (state)
this:
R = (SG, C)

goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
obtain SG' and C' where Rdef':"Rsubst R \<sigma> = (SG',C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>SG' C'. Rsubst R \<sigma> = (SG', C') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases R, auto)
[PROOF STATE]
proof (state)
this:
Rsubst R \<sigma> = (SG', C')

goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
obtain \<Gamma>C and \<Delta>C where Cdef:"C = (\<Gamma>C, \<Delta>C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Gamma>C \<Delta>C. C = (\<Gamma>C, \<Delta>C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases C, auto)
[PROOF STATE]
proof (state)
this:
C = (\<Gamma>C, \<Delta>C)

goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
obtain \<Gamma>C' and \<Delta>C' where C'def:"C' = (\<Gamma>C', \<Delta>C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Gamma>C' \<Delta>C'. C' = (\<Gamma>C', \<Delta>C') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases C', auto)
[PROOF STATE]
proof (state)
this:
C' = (\<Gamma>C', \<Delta>C')

goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
have CC':"(Ssubst (\<Gamma>C, \<Delta>C) \<sigma>) = (\<Gamma>C', \<Delta>C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ssubst (\<Gamma>C, \<Delta>C) \<sigma> = (\<Gamma>C', \<Delta>C')
[PROOF STEP]
using Rdef Rdef' Cdef C'def
[PROOF STATE]
proof (prove)
using this:
R = (SG, C)
Rsubst R \<sigma> = (SG', C')
C = (\<Gamma>C, \<Delta>C)
C' = (\<Gamma>C', \<Delta>C')

goal (1 subgoal):
 1. Ssubst (\<Gamma>C, \<Delta>C) \<sigma> = (\<Gamma>C', \<Delta>C')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ssubst (\<Gamma>C, \<Delta>C) \<sigma> = (\<Gamma>C', \<Delta>C')

goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
have "\<And>I \<nu>. is_interp I \<Longrightarrow> (\<And>\<Gamma> \<Delta> \<omega>  . List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)) \<Longrightarrow> \<nu> \<in> seq_sem I C'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
fix I::"('sf,'sc,'sz) interp" and \<nu>::"'sz state"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
assume good_interp:"is_interp I"
[PROOF STATE]
proof (state)
this:
is_interp I

goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
assume prems:"(\<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>))"
[PROOF STATE]
proof (state)
this:
List.member SG' (?\<Gamma>7, ?\<Delta>7) \<Longrightarrow> ?\<omega>7 \<in> seq_sem I (?\<Gamma>7, ?\<Delta>7)

goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
have good_interp':"\<And>\<omega>. is_interp (adjoint I \<sigma> \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<omega>. is_interp (local.adjoint I \<sigma> \<omega>)
[PROOF STEP]
using adjoint_safe[OF good_interp ] ssafe[unfolded ssafe_def]
[PROOF STATE]
proof (prove)
using this:
(\<And>i f'. SFunctions ?\<sigma> i = Some f' \<Longrightarrow> dfree f') \<Longrightarrow> is_interp (local.adjoint I ?\<sigma> ?\<nu>)
(\<forall>i f'. SFunctions \<sigma> i = Some f' \<longrightarrow> dfree f') \<and> (\<forall>f f'. SPredicates \<sigma> f = Some f' \<longrightarrow> fsafe f') \<and> (\<forall>f f'. SPrograms \<sigma> f = Some f' \<longrightarrow> hpsafe f') \<and> (\<forall>f f'. SODEs \<sigma> f = Some f' \<longrightarrow> osafe f') \<and> (\<forall>C C'. SContexts \<sigma> C = Some C' \<longrightarrow> fsafe C')

goal (1 subgoal):
 1. \<And>\<omega>. is_interp (local.adjoint I \<sigma> \<omega>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_interp (local.adjoint I \<sigma> ?\<omega>7)

goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
have sound:"\<And>\<omega>. (\<And>\<phi> \<nu> . List.member SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem (adjoint I \<sigma> \<omega>) \<phi>) \<Longrightarrow> \<omega> \<in> seq_sem (adjoint I \<sigma> \<omega>) (\<Gamma>C, \<Delta>C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<omega>. (\<And>\<phi> \<nu>. List.member SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem (local.adjoint I \<sigma> \<omega>) \<phi>) \<Longrightarrow> \<omega> \<in> seq_sem (local.adjoint I \<sigma> \<omega>) (\<Gamma>C, \<Delta>C)
[PROOF STEP]
using soundD_memv[of SG C] sound good_interp' Rdef Cdef
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sound (SG, C); is_interp ?I; \<And>\<phi> \<nu>. List.member SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem ?I \<phi>\<rbrakk> \<Longrightarrow> ?\<nu> \<in> seq_sem ?I C
sound R
is_interp (local.adjoint I \<sigma> ?\<omega>7)
R = (SG, C)
C = (\<Gamma>C, \<Delta>C)

goal (1 subgoal):
 1. \<And>\<omega>. (\<And>\<phi> \<nu>. List.member SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem (local.adjoint I \<sigma> \<omega>) \<phi>) \<Longrightarrow> \<omega> \<in> seq_sem (local.adjoint I \<sigma> \<omega>) (\<Gamma>C, \<Delta>C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<And>\<phi> \<nu>. List.member SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem (local.adjoint I \<sigma> ?\<omega>7) \<phi>) \<Longrightarrow> ?\<omega>7 \<in> seq_sem (local.adjoint I \<sigma> ?\<omega>7) (\<Gamma>C, \<Delta>C)

goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
have SadmitC:"Sadmit \<sigma> (\<Gamma>C, \<Delta>C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sadmit \<sigma> (\<Gamma>C, \<Delta>C)
[PROOF STEP]
using Radmit
[PROOF STATE]
proof (prove)
using this:
Radmit \<sigma> R

goal (1 subgoal):
 1. Sadmit \<sigma> (\<Gamma>C, \<Delta>C)
[PROOF STEP]
unfolding Radmit_def Rdef Cdef
[PROOF STATE]
proof (prove)
using this:
(\<forall>i\<ge>0. i < length (fst (SG, \<Gamma>C, \<Delta>C)) \<longrightarrow> Sadmit \<sigma> (fst (SG, \<Gamma>C, \<Delta>C) ! i)) \<and> Sadmit \<sigma> (snd (SG, \<Gamma>C, \<Delta>C))

goal (1 subgoal):
 1. Sadmit \<sigma> (\<Gamma>C, \<Delta>C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sadmit \<sigma> (\<Gamma>C, \<Delta>C)

goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
have SsafeC:"Ssafe (\<Gamma>C, \<Delta>C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ssafe (\<Gamma>C, \<Delta>C)
[PROOF STEP]
using Rsafe
[PROOF STATE]
proof (prove)
using this:
Rsafe R

goal (1 subgoal):
 1. Ssafe (\<Gamma>C, \<Delta>C)
[PROOF STEP]
unfolding Rsafe_def Rdef Cdef
[PROOF STATE]
proof (prove)
using this:
(\<forall>i\<ge>0. i < length (fst (SG, \<Gamma>C, \<Delta>C)) \<longrightarrow> Ssafe (fst (SG, \<Gamma>C, \<Delta>C) ! i)) \<and> Ssafe (snd (SG, \<Gamma>C, \<Delta>C))

goal (1 subgoal):
 1. Ssafe (\<Gamma>C, \<Delta>C)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ssafe (\<Gamma>C, \<Delta>C)

goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
have seq_sem:"\<nu> \<in> seq_sem (adjoint I \<sigma> \<nu>) (\<Gamma>C, \<Delta>C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>C, \<Delta>C)
[PROOF STEP]
proof(rule sound)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
fix S :: "('sf,'sc,'sz) sequent" and \<nu>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
assume mem:"List.member SG S"
[PROOF STATE]
proof (state)
this:
List.member SG S

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
obtain \<Gamma>S \<Delta>S where Sdef:"S = (\<Gamma>S, \<Delta>S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Gamma>S \<Delta>S. S = (\<Gamma>S, \<Delta>S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases S, auto)
[PROOF STATE]
proof (state)
this:
S = (\<Gamma>S, \<Delta>S)

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
from mem
[PROOF STATE]
proof (chain)
picking this:
List.member SG S
[PROOF STEP]
obtain di where di:"di < length SG \<and> SG ! di = S"
[PROOF STATE]
proof (prove)
using this:
List.member SG S

goal (1 subgoal):
 1. (\<And>di. di < length SG \<and> SG ! di = S \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson in_set_conv_nth in_set_member)
[PROOF STATE]
proof (state)
this:
di < length SG \<and> SG ! di = S

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
have SadmitS:"Sadmit \<sigma> (\<Gamma>S, \<Delta>S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sadmit \<sigma> (\<Gamma>S, \<Delta>S)
[PROOF STEP]
using Rdef Sdef di Radmit Radmit_def
[PROOF STATE]
proof (prove)
using this:
R = (SG, C)
S = (\<Gamma>S, \<Delta>S)
di < length SG \<and> SG ! di = S
Radmit \<sigma> R
Radmit ?\<sigma> ?R = ((\<forall>i\<ge>0. i < length (fst ?R) \<longrightarrow> Sadmit ?\<sigma> (fst ?R ! i)) \<and> Sadmit ?\<sigma> (snd ?R))

goal (1 subgoal):
 1. Sadmit \<sigma> (\<Gamma>S, \<Delta>S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sadmit \<sigma> (\<Gamma>S, \<Delta>S)

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
have SsafeS:"Ssafe (\<Gamma>S, \<Delta>S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ssafe (\<Gamma>S, \<Delta>S)
[PROOF STEP]
using Rsafe
[PROOF STATE]
proof (prove)
using this:
Rsafe R

goal (1 subgoal):
 1. Ssafe (\<Gamma>S, \<Delta>S)
[PROOF STEP]
unfolding Rsafe_def Rdef Cdef
[PROOF STATE]
proof (prove)
using this:
(\<forall>i\<ge>0. i < length (fst (SG, \<Gamma>C, \<Delta>C)) \<longrightarrow> Ssafe (fst (SG, \<Gamma>C, \<Delta>C) ! i)) \<and> Ssafe (snd (SG, \<Gamma>C, \<Delta>C))

goal (1 subgoal):
 1. Ssafe (\<Gamma>S, \<Delta>S)
[PROOF STEP]
using Sdef mem di
[PROOF STATE]
proof (prove)
using this:
(\<forall>i\<ge>0. i < length (fst (SG, \<Gamma>C, \<Delta>C)) \<longrightarrow> Ssafe (fst (SG, \<Gamma>C, \<Delta>C) ! i)) \<and> Ssafe (snd (SG, \<Gamma>C, \<Delta>C))
S = (\<Gamma>S, \<Delta>S)
List.member SG S
di < length SG \<and> SG ! di = S

goal (1 subgoal):
 1. Ssafe (\<Gamma>S, \<Delta>S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ssafe (\<Gamma>S, \<Delta>S)

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
have map_mem:"\<And>f L x. List.member L x \<Longrightarrow> List.member (map f L) (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f L x. List.member L x \<Longrightarrow> List.member (map f L) (f x)
[PROOF STEP]
subgoal for f L x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List.member L x \<Longrightarrow> List.member (map f L) (f x)
[PROOF STEP]
by (induction L, auto simp add: member_rec)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
List.member ?L7 ?x7 \<Longrightarrow> List.member (map ?f7 ?L7) (?f7 ?x7)

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
let ?S' = "(Ssubst (\<Gamma>S, \<Delta>S) \<sigma>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
have eq:"Ssubst S \<sigma> = (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>S, map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ssubst S \<sigma> = (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>S, map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>S)
[PROOF STEP]
using Sdef
[PROOF STATE]
proof (prove)
using this:
S = (\<Gamma>S, \<Delta>S)

goal (1 subgoal):
 1. Ssubst S \<sigma> = (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>S, map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>S)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ssubst S \<sigma> = (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>S, map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>S)

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
from Sdef
[PROOF STATE]
proof (chain)
picking this:
S = (\<Gamma>S, \<Delta>S)
[PROOF STEP]
have mem':"List.member SG' (fst ?S', snd ?S')"
[PROOF STATE]
proof (prove)
using this:
S = (\<Gamma>S, \<Delta>S)

goal (1 subgoal):
 1. List.member SG' (fst (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>), snd (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>))
[PROOF STEP]
using mem Rdef Rdef' eq map_mem[of SG S "(\<lambda>x. Ssubst x \<sigma>)"]
[PROOF STATE]
proof (prove)
using this:
S = (\<Gamma>S, \<Delta>S)
List.member SG S
R = (SG, C)
Rsubst R \<sigma> = (SG', C')
Ssubst S \<sigma> = (map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Gamma>S, map (\<lambda>\<phi>. Fsubst \<phi> \<sigma>) \<Delta>S)
List.member SG S \<Longrightarrow> List.member (map (\<lambda>x. Ssubst x \<sigma>) SG) (Ssubst S \<sigma>)

goal (1 subgoal):
 1. List.member SG' (fst (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>), snd (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
List.member SG' (fst (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>), snd (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>))

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
have "\<nu>' \<in> seq_sem I (fst ?S', snd ?S')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>' \<in> seq_sem I (fst (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>), snd (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>))
[PROOF STEP]
by (rule prems[OF mem', of \<nu>'])
[PROOF STATE]
proof (state)
this:
\<nu>' \<in> seq_sem I (fst (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>), snd (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>))

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nu>' \<in> seq_sem I (fst (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>), snd (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>))
[PROOF STEP]
have "\<nu>' \<in> seq_sem (adjoint I \<sigma> \<nu>') S"
[PROOF STATE]
proof (prove)
using this:
\<nu>' \<in> seq_sem I (fst (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>), snd (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>))

goal (1 subgoal):
 1. \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>') S
[PROOF STEP]
using subst_sequent[OF good_interp SadmitS SsafeS ssafe, of \<nu>']
        Sdef
[PROOF STATE]
proof (prove)
using this:
\<nu>' \<in> seq_sem I (fst (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>), snd (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>))
(\<nu>' \<in> seq_sem I (Ssubst (\<Gamma>S, \<Delta>S) \<sigma>)) = (\<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>') (\<Gamma>S, \<Delta>S))
S = (\<Gamma>S, \<Delta>S)

goal (1 subgoal):
 1. \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>') S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>') S

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
have VA:"Vagree \<nu> \<nu>' (FVS \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Vagree \<nu> \<nu>' (FVS \<sigma>)
[PROOF STEP]
using FVS
[PROOF STATE]
proof (prove)
using this:
FVS \<sigma> = {}

goal (1 subgoal):
 1. Vagree \<nu> \<nu>' (FVS \<sigma>)
[PROOF STEP]
unfolding Vagree_def
[PROOF STATE]
proof (prove)
using this:
FVS \<sigma> = {}

goal (1 subgoal):
 1. (\<forall>i. Inl i \<in> FVS \<sigma> \<longrightarrow> fst \<nu> $ i = fst \<nu>' $ i) \<and> (\<forall>i. Inr i \<in> FVS \<sigma> \<longrightarrow> snd \<nu> $ i = snd \<nu>' $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Vagree \<nu> \<nu>' (FVS \<sigma>)

goal (1 subgoal):
 1. \<And>\<phi> \<nu>'. List.member SG \<phi> \<Longrightarrow> \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) \<phi>
[PROOF STEP]
show "\<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) S
[PROOF STEP]
using adjoint_consequence VA ssafe[unfolded ssafe_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>f f'. SFunctions ?\<sigma> f = Some f' \<Longrightarrow> dsafe f'; \<And>f f'. SPredicates ?\<sigma> f = Some f' \<Longrightarrow> fsafe f'; Vagree ?\<nu> ?\<omega> (FVS ?\<sigma>)\<rbrakk> \<Longrightarrow> local.adjoint ?I ?\<sigma> ?\<nu> = local.adjoint ?I ?\<sigma> ?\<omega>
Vagree \<nu> \<nu>' (FVS \<sigma>)
(\<forall>i f'. SFunctions \<sigma> i = Some f' \<longrightarrow> dfree f') \<and> (\<forall>f f'. SPredicates \<sigma> f = Some f' \<longrightarrow> fsafe f') \<and> (\<forall>f f'. SPrograms \<sigma> f = Some f' \<longrightarrow> hpsafe f') \<and> (\<forall>f f'. SODEs \<sigma> f = Some f' \<longrightarrow> osafe f') \<and> (\<forall>C C'. SContexts \<sigma> C = Some C' \<longrightarrow> fsafe C')

goal (1 subgoal):
 1. \<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) S
[PROOF STEP]
by (metis \<open>\<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>') S\<close> dfree_is_dsafe)
[PROOF STATE]
proof (state)
this:
\<nu>' \<in> seq_sem (local.adjoint I \<sigma> \<nu>) S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>C, \<Delta>C)

goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
have "\<nu> \<in> seq_sem I (\<Gamma>C', \<Delta>C')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> \<in> seq_sem I (\<Gamma>C', \<Delta>C')
[PROOF STEP]
using subst_sequent[OF good_interp SadmitC SsafeC ssafe, of \<nu>] seq_sem Cdef C'def CC'
[PROOF STATE]
proof (prove)
using this:
(\<nu> \<in> seq_sem I (Ssubst (\<Gamma>C, \<Delta>C) \<sigma>)) = (\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>C, \<Delta>C))
\<nu> \<in> seq_sem (local.adjoint I \<sigma> \<nu>) (\<Gamma>C, \<Delta>C)
C = (\<Gamma>C, \<Delta>C)
C' = (\<Gamma>C', \<Delta>C')
Ssubst (\<Gamma>C, \<Delta>C) \<sigma> = (\<Gamma>C', \<Delta>C')

goal (1 subgoal):
 1. \<nu> \<in> seq_sem I (\<Gamma>C', \<Delta>C')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nu> \<in> seq_sem I (\<Gamma>C', \<Delta>C')

goal (1 subgoal):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<nu> \<in> seq_sem I C'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nu> \<in> seq_sem I (\<Gamma>C', \<Delta>C')
[PROOF STEP]
show  "\<nu> \<in> seq_sem I C'"
[PROOF STATE]
proof (prove)
using this:
\<nu> \<in> seq_sem I (\<Gamma>C', \<Delta>C')

goal (1 subgoal):
 1. \<nu> \<in> seq_sem I C'
[PROOF STEP]
using C'def
[PROOF STATE]
proof (prove)
using this:
\<nu> \<in> seq_sem I (\<Gamma>C', \<Delta>C')
C' = (\<Gamma>C', \<Delta>C')

goal (1 subgoal):
 1. \<nu> \<in> seq_sem I C'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nu> \<in> seq_sem I C'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_interp ?I7; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem ?I7 (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> ?\<nu>7 \<in> seq_sem ?I7 C'

goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_interp ?I7; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem ?I7 (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> ?\<nu>7 \<in> seq_sem ?I7 C'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_interp ?I7; \<And>\<Gamma> \<Delta> \<omega>. List.member SG' (\<Gamma>, \<Delta>) \<Longrightarrow> \<omega> \<in> seq_sem ?I7 (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> ?\<nu>7 \<in> seq_sem ?I7 C'

goal (1 subgoal):
 1. sound (Rsubst R \<sigma>)
[PROOF STEP]
apply(rule soundI_memv')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<phi> \<nu>. List.member ?SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem I \<phi>\<rbrakk> \<Longrightarrow> is_interp I
 2. \<And>I \<nu> \<Gamma> \<Delta> \<omega>. \<lbrakk>is_interp I; \<And>\<phi> \<nu>. List.member ?SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem I \<phi>; List.member SG' (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)
 3. Rsubst R \<sigma> = (?SG, C')
[PROOF STEP]
using Rdef'
[PROOF STATE]
proof (prove)
using this:
Rsubst R \<sigma> = (SG', C')

goal (3 subgoals):
 1. \<And>I \<nu>. \<lbrakk>is_interp I; \<And>\<phi> \<nu>. List.member ?SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem I \<phi>\<rbrakk> \<Longrightarrow> is_interp I
 2. \<And>I \<nu> \<Gamma> \<Delta> \<omega>. \<lbrakk>is_interp I; \<And>\<phi> \<nu>. List.member ?SG \<phi> \<Longrightarrow> \<nu> \<in> seq_sem I \<phi>; List.member SG' (\<Gamma>, \<Delta>)\<rbrakk> \<Longrightarrow> \<omega> \<in> seq_sem I (\<Gamma>, \<Delta>)
 3. Rsubst R \<sigma> = (?SG, C')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sound (Rsubst R \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_object_value_invariant:
  shows "atomic_step_invariant s = atomic_step_invariant (set_object_value ob va s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant s = atomic_step_invariant (set_object_value ob va s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant s = atomic_step_invariant (set_object_value ob va s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant s = atomic_step_invariant (set_object_value ob va s)
[PROOF STEP]
unfolding atomic_step_invariant_def atomic_step_precondition_def ipc_precondition_def
      sp_subset_def set_object_value_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>p1 p2. sp_impl_subj_subj s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)) = ((\<forall>p1 p2. sp_impl_subj_subj (s\<lparr>obj := (obj s)(ob := va)\<rparr>) p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj (s\<lparr>obj := (obj s)(ob := va)\<rparr>) p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m))
[PROOF STEP]
by (simp split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits)
[PROOF STATE]
proof (state)
this:
atomic_step_invariant s = atomic_step_invariant (set_object_value ob va s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_thread_value_invariant:
  shows "atomic_step_invariant s = atomic_step_invariant (s \<lparr> thread := thrst \<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant s = atomic_step_invariant (s\<lparr>thread := thrst\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant s = atomic_step_invariant (s\<lparr>thread := thrst\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant s = atomic_step_invariant (s\<lparr>thread := thrst\<rparr>)
[PROOF STEP]
unfolding atomic_step_invariant_def atomic_step_precondition_def ipc_precondition_def
      sp_subset_def set_object_value_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>p1 p2. sp_impl_subj_subj s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)) = ((\<forall>p1 p2. sp_impl_subj_subj (s\<lparr>thread := thrst\<rparr>) p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj (s\<lparr>thread := thrst\<rparr>) p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m))
[PROOF STEP]
by (simp split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits)
[PROOF STATE]
proof (state)
this:
atomic_step_invariant s = atomic_step_invariant (s\<lparr>thread := thrst\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atomic_ipc_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
proof (cases stage)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. stage = PREP \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
 2. stage = WAIT \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
 3. \<And>x3. stage = BUF x3 \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
case PREP
[PROOF STATE]
proof (state)
this:
stage = PREP

goal (3 subgoals):
 1. stage = PREP \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
 2. stage = WAIT \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
 3. \<And>x3. stage = BUF x3 \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
stage = PREP
atomic_step_invariant s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stage = PREP
atomic_step_invariant s

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
unfolding atomic_step_ipc_def atomic_step_invariant_def
[PROOF STATE]
proof (prove)
using this:
stage = PREP
sp_subset s

goal (1 subgoal):
 1. sp_subset (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> set_object_value (PAGE page') (obj s (PAGE page)) s | RECV \<Rightarrow> s | _ \<Rightarrow> s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)

goal (2 subgoals):
 1. stage = WAIT \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
 2. \<And>x3. stage = BUF x3 \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. stage = WAIT \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
 2. \<And>x3. stage = BUF x3 \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
case WAIT
[PROOF STATE]
proof (state)
this:
stage = WAIT

goal (2 subgoals):
 1. stage = WAIT \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
 2. \<And>x3. stage = BUF x3 \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
stage = WAIT
atomic_step_invariant s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stage = WAIT
atomic_step_invariant s

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
unfolding atomic_step_ipc_def atomic_step_invariant_def
[PROOF STATE]
proof (prove)
using this:
stage = WAIT
sp_subset s

goal (1 subgoal):
 1. sp_subset (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> set_object_value (PAGE page') (obj s (PAGE page)) s | RECV \<Rightarrow> s | _ \<Rightarrow> s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)

goal (1 subgoal):
 1. \<And>x3. stage = BUF x3 \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x3. stage = BUF x3 \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
case BUF
[PROOF STATE]
proof (state)
this:
stage = BUF x3_

goal (1 subgoal):
 1. \<And>x3. stage = BUF x3 \<Longrightarrow> atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
using assms BUF set_object_value_invariant
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant s
stage = BUF x3_
atomic_step_invariant ?s = atomic_step_invariant (set_object_value ?ob ?va ?s)

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)
[PROOF STEP]
unfolding atomic_step_ipc_def
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant s
stage = BUF x3_
atomic_step_invariant ?s = atomic_step_invariant (set_object_value ?ob ?va ?s)

goal (1 subgoal):
 1. atomic_step_invariant (case stage of BUF page' \<Rightarrow> case dir of SEND \<Rightarrow> set_object_value (PAGE page') (obj s (PAGE page)) s | RECV \<Rightarrow> s | _ \<Rightarrow> s)
[PROOF STEP]
by (simp split: ipc_direction_t.splits)
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atomic_ev_wait_one_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step_ev_wait_one tid s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_wait_one tid s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_wait_one tid s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
atomic_step_invariant s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant s

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_wait_one tid s)
[PROOF STEP]
unfolding atomic_step_ev_wait_one_def atomic_step_invariant_def sp_subset_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>p1 p2. sp_impl_subj_subj s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)

goal (1 subgoal):
 1. (\<forall>p1 p2. sp_impl_subj_subj (s\<lparr>thread := (thread s)(tid := thread s tid\<lparr>ev_counter := ev_counter (thread s tid) - 1\<rparr>)\<rparr>) p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj (s\<lparr>thread := (thread s)(tid := thread s tid\<lparr>ev_counter := ev_counter (thread s tid) - 1\<rparr>)\<rparr>) p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step_ev_wait_one tid s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atomic_ev_wait_all_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step_ev_wait_all tid s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_wait_all tid s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_wait_all tid s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
atomic_step_invariant s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant s

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_wait_all tid s)
[PROOF STEP]
unfolding atomic_step_ev_wait_all_def atomic_step_invariant_def sp_subset_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>p1 p2. sp_impl_subj_subj s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)

goal (1 subgoal):
 1. (\<forall>p1 p2. sp_impl_subj_subj (s\<lparr>thread := (thread s)(tid := thread s tid\<lparr>ev_counter := 0\<rparr>)\<rparr>) p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj (s\<lparr>thread := (thread s)(tid := thread s tid\<lparr>ev_counter := 0\<rparr>)\<rparr>) p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step_ev_wait_all tid s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atomic_ev_signal_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step_ev_signal tid  partner s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_signal tid partner s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_signal tid partner s)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
atomic_step_invariant s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant s

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step_ev_signal tid partner s)
[PROOF STEP]
unfolding atomic_step_ev_signal_def atomic_step_invariant_def sp_subset_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>p1 p2. sp_impl_subj_subj s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)

goal (1 subgoal):
 1. (\<forall>p1 p2. sp_impl_subj_subj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj (s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr>) p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step_ev_signal tid partner s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem atomic_step_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step s a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (atomic_step s a)
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. a = SK_IPC x11 x12 x13 x14 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 3. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 4. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
case SK_IPC
[PROOF STATE]
proof (state)
this:
a = SK_IPC x11_ x12_ x13_ x14_

goal (4 subgoals):
 1. \<And>x11 x12 x13 x14. a = SK_IPC x11 x12 x13 x14 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 3. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 4. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = SK_IPC x11_ x12_ x13_ x14_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = SK_IPC x11_ x12_ x13_ x14_

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step s a)
[PROOF STEP]
unfolding atomic_step_def
[PROOF STATE]
proof (prove)
using this:
a = SK_IPC x11_ x12_ x13_ x14_

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
using assms atomic_ipc_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
a = SK_IPC x11_ x12_ x13_ x14_
atomic_step_invariant s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step_ipc ?tid ?dir ?stage ?partner ?page ?s)

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step s a)

goal (3 subgoals):
 1. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 3. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 3. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
case (SK_EV_WAIT ev_wait_stage consume)
[PROOF STATE]
proof (state)
this:
a = SK_EV_WAIT ev_wait_stage consume

goal (3 subgoals):
 1. \<And>x21 x22. a = SK_EV_WAIT x21 x22 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 3. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = SK_EV_WAIT ev_wait_stage consume
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = SK_EV_WAIT ev_wait_stage consume

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step s a)
[PROOF STEP]
proof (cases consume)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a = SK_EV_WAIT ev_wait_stage consume; consume = EV_CONSUME_ALL\<rbrakk> \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. \<lbrakk>a = SK_EV_WAIT ev_wait_stage consume; consume = EV_CONSUME_ONE\<rbrakk> \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
case EV_CONSUME_ALL
[PROOF STATE]
proof (state)
this:
consume = EV_CONSUME_ALL

goal (2 subgoals):
 1. \<lbrakk>a = SK_EV_WAIT ev_wait_stage consume; consume = EV_CONSUME_ALL\<rbrakk> \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. \<lbrakk>a = SK_EV_WAIT ev_wait_stage consume; consume = EV_CONSUME_ONE\<rbrakk> \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
consume = EV_CONSUME_ALL
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
consume = EV_CONSUME_ALL

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step s a)
[PROOF STEP]
unfolding atomic_step_def
[PROOF STATE]
proof (prove)
using this:
consume = EV_CONSUME_ALL

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
using SK_EV_WAIT assms atomic_ev_wait_all_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
consume = EV_CONSUME_ALL
a = SK_EV_WAIT ev_wait_stage consume
atomic_step_invariant s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step_ev_wait_all ?tid ?s)

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
by (simp split: ev_wait_stage_t.splits)
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step s a)

goal (1 subgoal):
 1. \<lbrakk>a = SK_EV_WAIT ev_wait_stage consume; consume = EV_CONSUME_ONE\<rbrakk> \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a = SK_EV_WAIT ev_wait_stage consume; consume = EV_CONSUME_ONE\<rbrakk> \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
case EV_CONSUME_ONE
[PROOF STATE]
proof (state)
this:
consume = EV_CONSUME_ONE

goal (1 subgoal):
 1. \<lbrakk>a = SK_EV_WAIT ev_wait_stage consume; consume = EV_CONSUME_ONE\<rbrakk> \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
consume = EV_CONSUME_ONE
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
consume = EV_CONSUME_ONE

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step s a)
[PROOF STEP]
unfolding atomic_step_def
[PROOF STATE]
proof (prove)
using this:
consume = EV_CONSUME_ONE

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
using SK_EV_WAIT assms atomic_ev_wait_one_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
consume = EV_CONSUME_ONE
a = SK_EV_WAIT ev_wait_stage consume
atomic_step_invariant s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step_ev_wait_one ?tid ?s)

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
by (simp split: ev_wait_stage_t.splits)
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step s a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step s a)

goal (2 subgoals):
 1. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
case SK_EV_SIGNAL
[PROOF STATE]
proof (state)
this:
a = SK_EV_SIGNAL x31_ x32_

goal (2 subgoals):
 1. \<And>x31 x32. a = SK_EV_SIGNAL x31 x32 \<Longrightarrow> atomic_step_invariant (atomic_step s a)
 2. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = SK_EV_SIGNAL x31_ x32_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = SK_EV_SIGNAL x31_ x32_

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step s a)
[PROOF STEP]
unfolding atomic_step_def
[PROOF STATE]
proof (prove)
using this:
a = SK_EV_SIGNAL x31_ x32_

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
using assms atomic_ev_signal_preserves_invariants
[PROOF STATE]
proof (prove)
using this:
a = SK_EV_SIGNAL x31_ x32_
atomic_step_invariant s
atomic_step_invariant ?s \<Longrightarrow> atomic_step_invariant (atomic_step_ev_signal ?tid ?partner ?s)

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
by (simp add: ev_signal_stage_t.splits)
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step s a)

goal (1 subgoal):
 1. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
case NONE
[PROOF STATE]
proof (state)
this:
a = NONE

goal (1 subgoal):
 1. a = NONE \<Longrightarrow> atomic_step_invariant (atomic_step s a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = NONE
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = NONE

goal (1 subgoal):
 1. atomic_step_invariant (atomic_step s a)
[PROOF STEP]
unfolding atomic_step_def
[PROOF STATE]
proof (prove)
using this:
a = NONE

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = NONE
atomic_step_invariant s

goal (1 subgoal):
 1. atomic_step_invariant (case a of SK_IPC dir stage partner page \<Rightarrow> atomic_step_ipc (current s) dir stage partner page s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> atomic_step_ev_wait_all (current s) s | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> atomic_step_ev_wait_one (current s) s | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> atomic_step_ev_signal (current s) partner s | NONE \<Rightarrow> s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (atomic_step s a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem cswitch_preserves_invariants:
  fixes s :: state_t
    and new_current :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (s \<lparr> current := new_current \<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atomic_step_invariant (s\<lparr>current := new_current\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant (s\<lparr>current := new_current\<rparr>)
[PROOF STEP]
let ?s1 = "s \<lparr> current := new_current \<rparr>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atomic_step_invariant (s\<lparr>current := new_current\<rparr>)
[PROOF STEP]
have "sp_subset s = sp_subset ?s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sp_subset s = sp_subset (s\<lparr>current := new_current\<rparr>)
[PROOF STEP]
unfolding sp_subset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>p1 p2. sp_impl_subj_subj s p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj s p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m)) = ((\<forall>p1 p2. sp_impl_subj_subj (s\<lparr>current := new_current\<rparr>) p1 p2 \<longrightarrow> Policy.sp_spec_subj_subj p1 p2) \<and> (\<forall>p1 p2 m. sp_impl_subj_obj (s\<lparr>current := new_current\<rparr>) p1 p2 m \<longrightarrow> Policy.sp_spec_subj_obj p1 p2 m))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sp_subset s = sp_subset (s\<lparr>current := new_current\<rparr>)

goal (1 subgoal):
 1. atomic_step_invariant (s\<lparr>current := new_current\<rparr>)
[PROOF STEP]
from assms this
[PROOF STATE]
proof (chain)
picking this:
atomic_step_invariant s
sp_subset s = sp_subset (s\<lparr>current := new_current\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atomic_step_invariant s
sp_subset s = sp_subset (s\<lparr>current := new_current\<rparr>)

goal (1 subgoal):
 1. atomic_step_invariant (s\<lparr>current := new_current\<rparr>)
[PROOF STEP]
unfolding atomic_step_invariant_def
[PROOF STATE]
proof (prove)
using this:
sp_subset s
sp_subset s = sp_subset (s\<lparr>current := new_current\<rparr>)

goal (1 subgoal):
 1. sp_subset (s\<lparr>current := new_current\<rparr>)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
atomic_step_invariant (s\<lparr>current := new_current\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem atomic_step_does_not_change_current_thread:
  shows "current (atomic_step s ipt) = current s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current (atomic_step s ipt) = current s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. current (atomic_step s ipt) = current s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current (atomic_step s ipt) = current s
[PROOF STEP]
unfolding atomic_step_def
          and atomic_step_ipc_def
          and set_object_value_def Let_def
          and atomic_step_ev_wait_one_def atomic_step_ev_wait_all_def
          and atomic_step_ev_signal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. current (case ipt of SK_IPC SEND (BUF page') partner page \<Rightarrow> s\<lparr>obj := (obj s)(PAGE page' := obj s (PAGE page))\<rparr> | SK_IPC RECV (BUF page') partner page \<Rightarrow> s | SK_IPC dir _ partner page \<Rightarrow> s | SK_EV_WAIT EV_FINISH EV_CONSUME_ALL \<Rightarrow> s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := 0\<rparr>)\<rparr> | SK_EV_WAIT EV_FINISH EV_CONSUME_ONE \<Rightarrow> s\<lparr>thread := (thread s)(current s := thread s (current s)\<lparr>ev_counter := ev_counter (thread s (current s)) - 1\<rparr>)\<rparr> | SK_EV_WAIT _ consume \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_PREP partner \<Rightarrow> s | SK_EV_SIGNAL EV_SIGNAL_FINISH partner \<Rightarrow> s\<lparr>thread := (thread s)(partner := thread s partner\<lparr>ev_counter := Suc (ev_counter (thread s partner))\<rparr>)\<rparr> | NONE \<Rightarrow> s) = current s
[PROOF STEP]
by (simp split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits
                        ev_consume_t.splits ev_wait_stage_t.splits ev_signal_stage_t.splits)
[PROOF STATE]
proof (state)
this:
current (atomic_step s ipt) = current s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma freeIn_substInfinitesimalQuadratic :
  assumes "var \<notin> vars a"
    "var \<notin> vars b"
    "var \<notin> vars c"
    "var \<notin> vars d"
  shows "freeIn var (substInfinitesimalQuadratic var a b c d At)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
proof(cases At)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. At = Less x1 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 2. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 3. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 4. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
case (Less p)
[PROOF STATE]
proof (state)
this:
At = Less p

goal (4 subgoals):
 1. \<And>x1. At = Less x1 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 2. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 3. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 4. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
unfolding substInfinitesimalQuadratic.simps Less
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (quadratic_sub_fm var a b c d (convertDerivative var p))
[PROOF STEP]
apply(rule free_in_quad_fm[of var a b c d "(convertDerivative var p)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. var \<notin> vars a
 2. var \<notin> vars b
 3. var \<notin> vars c
 4. var \<notin> vars d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
var \<notin> vars a
var \<notin> vars b
var \<notin> vars c
var \<notin> vars d

goal (4 subgoals):
 1. var \<notin> vars a
 2. var \<notin> vars b
 3. var \<notin> vars c
 4. var \<notin> vars d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalQuadratic var a b c d At)

goal (3 subgoals):
 1. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 2. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 3. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 2. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 3. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
case (Eq p)
[PROOF STATE]
proof (state)
this:
At = Eq p

goal (3 subgoals):
 1. \<And>x2. At = Eq x2 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 2. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 3. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
At = Eq p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
At = Eq p

goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. At = Eq p \<Longrightarrow> freeIn var (list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]))
[PROOF STEP]
apply(rule freeIn_list_conj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. At = Eq p \<Longrightarrow> \<forall>f\<in>set (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]). freeIn var f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>At = Eq p; var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>At = Eq p; x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using not_in_isovarspar
[PROOF STATE]
proof (prove)
using this:
isolate_variable_sparse ?p ?var ?x = ?q \<Longrightarrow> ?var \<notin> vars ?q

goal (2 subgoals):
 1. \<lbrakk>At = Eq p; var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>At = Eq p; x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalQuadratic var a b c d At)

goal (2 subgoals):
 1. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 2. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 2. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
case (Leq p)
[PROOF STATE]
proof (state)
this:
At = Leq p

goal (2 subgoals):
 1. \<And>x3. At = Leq x3 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
 2. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
At = Leq p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
At = Leq p

goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
unfolding substInfinitesimalQuadratic.simps Leq freeIn.simps
[PROOF STATE]
proof (prove)
using this:
Leq p = Leq p

goal (1 subgoal):
 1. freeIn var (allZero p var) \<and> freeIn var (quadratic_sub_fm var a b c d (convertDerivative var p))
[PROOF STEP]
using free_in_quad_fm[of var a b c d "(convertDerivative var p)", OF assms]
[PROOF STATE]
proof (prove)
using this:
Leq p = Leq p
freeIn var (quadratic_sub_fm var a b c d (convertDerivative var p))

goal (1 subgoal):
 1. freeIn var (allZero p var) \<and> freeIn var (quadratic_sub_fm var a b c d (convertDerivative var p))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x. quadratic_sub (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (if MPoly_Type.degree p var = 0 then fm.Atom (Less p) else Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (convertDerivative var (derivative var p)))) 0) \<Longrightarrow> freeIn var (list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]))
[PROOF STEP]
apply(rule freeIn_list_conj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x. quadratic_sub (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (if MPoly_Type.degree p var = 0 then fm.Atom (Less p) else Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (convertDerivative var (derivative var p)))) 0) \<Longrightarrow> \<forall>f\<in>set (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]). freeIn var f
[PROOF STEP]
using not_in_isovarspar
[PROOF STATE]
proof (prove)
using this:
isolate_variable_sparse ?p ?var ?x = ?q \<Longrightarrow> ?var \<notin> vars ?q

goal (1 subgoal):
 1. freeIn var (liftmap (\<lambda>x. quadratic_sub (var + x) (liftPoly 0 x a) (liftPoly 0 x b) (liftPoly 0 x c) (liftPoly 0 x d)) (if MPoly_Type.degree p var = 0 then fm.Atom (Less p) else Or (fm.Atom (Less p)) (And (fm.Atom (Eq p)) (convertDerivative var (derivative var p)))) 0) \<Longrightarrow> \<forall>f\<in>set (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]). freeIn var f
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalQuadratic var a b c d At)

goal (1 subgoal):
 1. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
case (Neq p)
[PROOF STATE]
proof (state)
this:
At = Neq p

goal (1 subgoal):
 1. \<And>x4. At = Neq x4 \<Longrightarrow> freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
At = Neq p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
At = Neq p

goal (1 subgoal):
 1. freeIn var (substInfinitesimalQuadratic var a b c d At)
[PROOF STEP]
apply (auto simp add:neg_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF\<rbrakk> \<Longrightarrow> freeIn var (list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]))
[PROOF STEP]
apply(rule freeIn_list_conj)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF\<rbrakk> \<Longrightarrow> \<forall>f\<in>set (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]). freeIn var f
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF; var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF; x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using not_in_isovarspar
[PROOF STATE]
proof (prove)
using this:
isolate_variable_sparse ?p ?var ?x = ?q \<Longrightarrow> ?var \<notin> vars ?q

goal (2 subgoals):
 1. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF; var \<in> vars (isolate_variable_sparse p var (MPoly_Type.degree p var))\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>At = Neq p; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> FalseF; list_conj (map (\<lambda>i. fm.Atom (Eq (isolate_variable_sparse p var i))) [0..<MPoly_Type.degree p var] @ [fm.Atom (Eq (isolate_variable_sparse p var (MPoly_Type.degree p var)))]) \<noteq> TrueF; x < MPoly_Type.degree p var; var \<in> vars (isolate_variable_sparse p var x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
freeIn var (substInfinitesimalQuadratic var a b c d At)

goal:
No subgoals!
[PROOF STEP]
qed