theory SR_lemmas_C

lemma rf_sr_ctes_of_cliftE:
  assumes cof: "ctes_of s p = Some cte"
  assumes sr: "(s, s') \<in> rf_sr"
  and     rl: "\<And>cte' ctel'. \<lbrakk>ctes_of s p = Some (cte_to_H ctel');
                        cslift s' (Ptr p) = Some cte';
                        cte_lift cte' = Some ctel';
                        cte = cte_to_H ctel' ;
                        cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> R"
  shows "R" using sr cof apply - apply (frule (1) rf_sr_ctes_of_clift) apply (elim conjE exE) apply (rule rl) apply simp apply assumption apply clarsimp apply clarsimp apply (clarsimp simp: c_valid_cte_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
(s, s') \<in> rf_sr
ctes_of s p = Some cte

goal (1 subgoal):
 1. R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; \<exists>cte'. cslift s' (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> R proof (prove)
goal (5 subgoals):
 1. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> ctes_of s p = Some (cte_to_H (?ctel'9 cte'))
 2. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cslift s' (cte_Ptr p) = Some (?cte'9 cte')
 3. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cte_lift (?cte'9 cte') = Some (?ctel'9 cte')
 4. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cte = cte_to_H (?ctel'9 cte')
 5. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cl_valid_cte (?ctel'9 cte') proof (prove)
goal (4 subgoals):
 1. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cslift s' (cte_Ptr p) = Some (?cte'9 cte')
 2. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cte_lift (?cte'9 cte') = Some (the (cte_lift cte'))
 3. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cte = cte_to_H (the (cte_lift cte'))
 4. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cl_valid_cte (the (cte_lift cte')) proof (prove)
goal (3 subgoals):
 1. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cte_lift cte' = Some (the (cte_lift cte'))
 2. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cte = cte_to_H (the (cte_lift cte'))
 3. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cl_valid_cte (the (cte_lift cte')) proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cte = cte_to_H (the (cte_lift cte'))
 2. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cl_valid_cte (the (cte_lift cte')) proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s p = Some cte; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' \<noteq> None; cte = cte_to_H (the (cte_lift cte')); c_valid_cte cte'\<rbrakk> \<Longrightarrow> cl_valid_cte (the (cte_lift cte')) proof (prove)
goal:
No subgoals!