theory CSpace_R

lemma ghost_relation_of_heap:
  "ghost_relation h ups cns \<longleftrightarrow> ups_of_heap h = ups \<and> cns_of_heap h = cns" apply (rule iffI) apply (rule conjI) apply (rule ext) apply (clarsimp simp add: ghost_relation_def ups_of_heap_def) apply (drule_tac x=x in spec) apply (auto simp: ghost_relation_def ups_of_heap_def
                split: option.splits Structures_A.kernel_object.splits
                       arch_kernel_obj.splits)[1] subgoal for x dev sz by (drule_tac x = sz in spec,simp) apply (rule ext) apply (clarsimp simp add: ghost_relation_def cns_of_heap_def) apply (drule_tac x=x in spec)+ apply (rule ccontr) apply (simp split: option.splits Structures_A.kernel_object.splits
                      arch_kernel_obj.splits)[1] apply (simp split: if_split_asm) apply force apply (drule not_sym) apply clarsimp apply (erule_tac x=y in allE) apply simp apply (auto simp add: ghost_relation_def ups_of_heap_def cns_of_heap_def
              split: option.splits Structures_A.kernel_object.splits
                     arch_kernel_obj.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ghost_relation h ups cns = (ups_of_heap h = ups \<and> cns_of_heap h = cns) proof (prove)
goal (2 subgoals):
 1. ghost_relation h ups cns \<Longrightarrow> ups_of_heap h = ups \<and> cns_of_heap h = cns
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (3 subgoals):
 1. ghost_relation h ups cns \<Longrightarrow> ups_of_heap h = ups
 2. ghost_relation h ups cns \<Longrightarrow> cns_of_heap h = cns
 3. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (3 subgoals):
 1. \<And>x. ghost_relation h ups cns \<Longrightarrow> ups_of_heap h x = ups x
 2. ghost_relation h ups cns \<Longrightarrow> cns_of_heap h = cns
 3. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>a sz. (\<exists>dev. h a = Some (ArchObj (DataPage dev sz))) = (ups a = Some sz); \<forall>a n. (\<exists>cs. h a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns a = Some n)\<rbrakk> \<Longrightarrow> (case h x of None \<Rightarrow> None | Some (ArchObj (DataPage dev xa)) \<Rightarrow> Some xa | Some (ArchObj _) \<Rightarrow> None | Some _ \<Rightarrow> None) = ups x
 2. ghost_relation h ups cns \<Longrightarrow> cns_of_heap h = cns
 3. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>a n. (\<exists>cs. h a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns a = Some n); \<forall>sz. (\<exists>dev. h x = Some (ArchObj (DataPage dev sz))) = (ups x = Some sz)\<rbrakk> \<Longrightarrow> (case h x of None \<Rightarrow> None | Some (ArchObj (DataPage dev xa)) \<Rightarrow> Some xa | Some (ArchObj _) \<Rightarrow> None | Some _ \<Rightarrow> None) = ups x
 2. ghost_relation h ups cns \<Longrightarrow> cns_of_heap h = cns
 3. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (3 subgoals):
 1. \<And>x x41 x42. \<lbrakk>\<forall>a n. (\<exists>cs. h a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns a = Some n); \<forall>sz. (x42 = sz) = (ups x = Some sz); h x = Some (ArchObj (DataPage x41 x42))\<rbrakk> \<Longrightarrow> Some x42 = ups x
 2. ghost_relation h ups cns \<Longrightarrow> cns_of_heap h = cns
 3. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a n. (\<exists>cs. h a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns a = Some n); \<forall>sza. (sz = sza) = (ups x = Some sza); h x = Some (ArchObj (DataPage dev sz))\<rbrakk> \<Longrightarrow> Some sz = ups x proof (prove)
goal (2 subgoals):
 1. ghost_relation h ups cns \<Longrightarrow> cns_of_heap h = cns
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x. ghost_relation h ups cns \<Longrightarrow> cns_of_heap h x = cns x
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>a sz. (\<exists>dev. h a = Some (ArchObj (DataPage dev sz))) = (ups a = Some sz); \<forall>a n. (\<exists>cs. h a = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns a = Some n)\<rbrakk> \<Longrightarrow> (case h x of None \<Rightarrow> None | Some (CNode sz cs) \<Rightarrow> if well_formed_cnode_n sz cs then Some sz else None | Some _ \<Rightarrow> None) = cns x
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>sz. (\<exists>dev. h x = Some (ArchObj (DataPage dev sz))) = (ups x = Some sz); \<forall>n. (\<exists>cs. h x = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns x = Some n)\<rbrakk> \<Longrightarrow> (case h x of None \<Rightarrow> None | Some (CNode sz cs) \<Rightarrow> if well_formed_cnode_n sz cs then Some sz else None | Some _ \<Rightarrow> None) = cns x
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>sz. (\<exists>dev. h x = Some (ArchObj (DataPage dev sz))) = (ups x = Some sz); \<forall>n. (\<exists>cs. h x = Some (CNode n cs) \<and> well_formed_cnode_n n cs) = (cns x = Some n); (case h x of None \<Rightarrow> None | Some (CNode sz cs) \<Rightarrow> if well_formed_cnode_n sz cs then Some sz else None | Some _ \<Rightarrow> None) \<noteq> cns x\<rbrakk> \<Longrightarrow> False
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x x2 x11 x12. \<lbrakk>ups x = None; \<forall>n. (x11 = n \<and> well_formed_cnode_n n x12) = (cns x = Some n); h x = Some (CNode x11 x12); x2 = CNode x11 x12; (if well_formed_cnode_n x11 x12 then Some x11 else None) \<noteq> cns x\<rbrakk> \<Longrightarrow> False
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (3 subgoals):
 1. \<And>x x2 x11 x12. \<lbrakk>ups x = None; \<forall>n. (x11 = n \<and> well_formed_cnode_n n x12) = (cns x = Some n); h x = Some (CNode x11 x12); x2 = CNode x11 x12; well_formed_cnode_n x11 x12; Some x11 \<noteq> cns x\<rbrakk> \<Longrightarrow> False
 2. \<And>x x2 x11 x12. \<lbrakk>ups x = None; \<forall>n. (x11 = n \<and> well_formed_cnode_n n x12) = (cns x = Some n); h x = Some (CNode x11 x12); x2 = CNode x11 x12; \<not> well_formed_cnode_n x11 x12; None \<noteq> cns x\<rbrakk> \<Longrightarrow> False
 3. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x x2 x11 x12. \<lbrakk>ups x = None; \<forall>n. (x11 = n \<and> well_formed_cnode_n n x12) = (cns x = Some n); h x = Some (CNode x11 x12); x2 = CNode x11 x12; \<not> well_formed_cnode_n x11 x12; None \<noteq> cns x\<rbrakk> \<Longrightarrow> False
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x x2 x11 x12. \<lbrakk>ups x = None; \<forall>n. (x11 = n \<and> well_formed_cnode_n n x12) = (cns x = Some n); h x = Some (CNode x11 x12); x2 = CNode x11 x12; \<not> well_formed_cnode_n x11 x12; cns x \<noteq> None\<rbrakk> \<Longrightarrow> False
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x x11 x12 y. \<lbrakk>ups x = None; \<forall>n. (x11 = n \<and> well_formed_cnode_n n x12) = (y = n); h x = Some (CNode x11 x12); \<not> well_formed_cnode_n x11 x12; cns x = Some y\<rbrakk> \<Longrightarrow> False
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (2 subgoals):
 1. \<And>x x11 x12 y. \<lbrakk>ups x = None; h x = Some (CNode x11 x12); \<not> well_formed_cnode_n x11 x12; cns x = Some y; (x11 = y \<and> well_formed_cnode_n y x12) = (y = y)\<rbrakk> \<Longrightarrow> False
 2. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal (1 subgoal):
 1. ups_of_heap h = ups \<and> cns_of_heap h = cns \<Longrightarrow> ghost_relation h ups cns proof (prove)
goal:
No subgoals!