theory CNode_IF

lemma equiv_valid_inv_conj_lift:
  assumes P: "equiv_valid_inv I (\<lambda>s s'. P s s') g f"
      and P': "equiv_valid_inv I (\<lambda>s s'. P' s s') g f"
  shows "equiv_valid_inv I (\<lambda>s s'. P s s' \<and> P' s s') g f" apply (clarsimp simp add: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def) apply (frule_tac st = t and s = st in use_equiv_valid_inv[OF _ _ _ _ _ _ P]) apply fastforce+ apply (frule_tac st = t and s = st in use_equiv_valid_inv[OF _ _ _ _ _ _ P']) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I (\<lambda>s s'. P s s' \<and> P' s s') g f proof (prove)
goal (1 subgoal):
 1. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> P b ba \<and> P' b ba proof (prove)
goal (6 subgoals):
 1. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t\<rbrakk> \<Longrightarrow> ?y24 st t a b aa ba \<in> fst (f st)
 2. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t\<rbrakk> \<Longrightarrow> g st
 3. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t\<rbrakk> \<Longrightarrow> g t
 4. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t\<rbrakk> \<Longrightarrow> I st t
 5. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t\<rbrakk> \<Longrightarrow> P st t
 6. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t; fst (aa, ba) = fst (?y24 st t a b aa ba) \<and> P (snd (?y24 st t a b aa ba)) (snd (aa, ba)) \<and> I (snd (?y24 st t a b aa ba)) (snd (aa, ba))\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> P b ba \<and> P' b ba proof (prove)
goal (1 subgoal):
 1. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t; fst (aa, ba) = fst (a, b) \<and> P (snd (a, b)) (snd (aa, ba)) \<and> I (snd (a, b)) (snd (aa, ba))\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> P b ba \<and> P' b ba proof (prove)
goal (6 subgoals):
 1. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t; fst (aa, ba) = fst (a, b) \<and> P (snd (a, b)) (snd (aa, ba)) \<and> I (snd (a, b)) (snd (aa, ba))\<rbrakk> \<Longrightarrow> ?y42 st t a b aa ba \<in> fst (f st)
 2. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t; fst (aa, ba) = fst (a, b) \<and> P (snd (a, b)) (snd (aa, ba)) \<and> I (snd (a, b)) (snd (aa, ba))\<rbrakk> \<Longrightarrow> g st
 3. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t; fst (aa, ba) = fst (a, b) \<and> P (snd (a, b)) (snd (aa, ba)) \<and> I (snd (a, b)) (snd (aa, ba))\<rbrakk> \<Longrightarrow> g t
 4. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t; fst (aa, ba) = fst (a, b) \<and> P (snd (a, b)) (snd (aa, ba)) \<and> I (snd (a, b)) (snd (aa, ba))\<rbrakk> \<Longrightarrow> I st t
 5. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t; fst (aa, ba) = fst (a, b) \<and> P (snd (a, b)) (snd (aa, ba)) \<and> I (snd (a, b)) (snd (aa, ba))\<rbrakk> \<Longrightarrow> P' st t
 6. \<And>st t a b aa ba. \<lbrakk>(a, b) \<in> fst (f st); (aa, ba) \<in> fst (f t); g st; g t; I st t; P st t; P' st t; fst (aa, ba) = fst (a, b) \<and> P (snd (a, b)) (snd (aa, ba)) \<and> I (snd (a, b)) (snd (aa, ba)); fst (aa, ba) = fst (?y42 st t a b aa ba) \<and> P' (snd (?y42 st t a b aa ba)) (snd (aa, ba)) \<and> I (snd (?y42 st t a b aa ba)) (snd (aa, ba))\<rbrakk> \<Longrightarrow> a = aa \<and> I b ba \<and> P b ba \<and> P' b ba proof (prove)
goal:
No subgoals!