theory Dpolicy

lemma cdl_domains_of_state_transform:
  assumes e: "einvs s"
  shows "cdl_domains_of_state (transform s) = domains_of_state s" proof - { fix ptr d assume "(ptr, d) \<in> cdl_domains_of_state (transform s)" hence "(ptr, d) \<in> domains_of_state s" apply (cases) using e apply (clarsimp simp: transform_def transform_objects_def restrict_map_def
                     split: if_split_asm Structures_A.kernel_object.splits) apply (case_tac z, simp_all add: nat_split_conv_to_if
                               split: if_split_asm) prefer 2 apply (rename_tac arch_kernel_obj) apply (case_tac arch_kernel_obj; simp) apply (drule valid_etcbs_tcb_etcb [rotated], fastforce) apply clarsimp apply (rule domains_of_state_aux.intros, assumption) apply (clarsimp simp: transform_tcb_def transform_full_intent_def Let_def) apply (insert einvs_idle [OF e]) apply (insert einvs_idle_domain [OF e]) apply clarsimp apply (erule domains_of_state_aux.domtcbs) apply simp done } note a = this { fix ptr d assume "(ptr, d) \<in> domains_of_state s" hence "(ptr, d) \<in> cdl_domains_of_state (transform s)" apply cases apply (case_tac "ptr = idle_thread_ptr") apply (insert einvs_idle [OF e])[1] apply (insert einvs_idle_domain [OF e])[1] apply simp apply (rule domidle) apply (frule ekheap_kheap_dom) using e apply fastforce apply clarsimp apply (drule (1) cdl_objects_tcb) apply (insert einvs_idle [OF e])[1] apply simp apply (erule domtcbs) apply (clarsimp simp: transform_full_intent_def Let_def) done } note b = this show ?thesis apply (rule set_eqI) apply clarify apply (blast intro!: a b) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
this:
(ptr, d) \<in> cdl_domains_of_state (transform s)

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (prove)
using this:
(ptr, d) \<in> cdl_domains_of_state (transform s)

goal (1 subgoal):
 1. (ptr, d) \<in> domains_of_state s proof (prove)
goal (2 subgoals):
 1. \<And>cdl_tcb. \<lbrakk>cdl_objects (transform s) ptr = Some (Tcb cdl_tcb); d = cdl_tcb_domain cdl_tcb\<rbrakk> \<Longrightarrow> (ptr, d) \<in> domains_of_state s
 2. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (ptr, d) \<in> domains_of_state s proof (prove)
using this:
einvs s

goal (2 subgoals):
 1. \<And>cdl_tcb. \<lbrakk>cdl_objects (transform s) ptr = Some (Tcb cdl_tcb); d = cdl_tcb_domain cdl_tcb\<rbrakk> \<Longrightarrow> (ptr, d) \<in> domains_of_state s
 2. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (ptr, d) \<in> domains_of_state s proof (prove)
goal (2 subgoals):
 1. \<And>cdl_tcb z. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; kheap s ptr = Some z; transform_object (machine_state s) ptr (ekheap s ptr) z = Tcb cdl_tcb\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 2. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (ptr, d) \<in> domains_of_state s proof (prove)
goal (3 subgoals):
 1. \<And>cdl_tcb z x2. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; kheap s ptr = Some (TCB x2); (case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr x2 etcb) = Tcb cdl_tcb; z = TCB x2\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 2. \<And>cdl_tcb z x5. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj x5); transform_object (machine_state s) ptr (ekheap s ptr) (ArchObj x5) = Tcb cdl_tcb; z = ArchObj x5\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 3. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (3 subgoals):
 1. \<And>cdl_tcb z x5. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj x5); transform_object (machine_state s) ptr (ekheap s ptr) (ArchObj x5) = Tcb cdl_tcb; z = ArchObj x5\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 2. \<And>cdl_tcb z x2. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; kheap s ptr = Some (TCB x2); (case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr x2 etcb) = Tcb cdl_tcb; z = TCB x2\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 3. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (3 subgoals):
 1. \<And>cdl_tcb z arch_kernel_obj. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; kheap s ptr = Some (ArchObj arch_kernel_obj); transform_object (machine_state s) ptr (ekheap s ptr) (ArchObj arch_kernel_obj) = Tcb cdl_tcb; z = ArchObj arch_kernel_obj\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 2. \<And>cdl_tcb z x2. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; kheap s ptr = Some (TCB x2); (case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr x2 etcb) = Tcb cdl_tcb; z = TCB x2\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 3. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (2 subgoals):
 1. \<And>cdl_tcb z x2. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; kheap s ptr = Some (TCB x2); (case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr x2 etcb) = Tcb cdl_tcb; z = TCB x2\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 2. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (2 subgoals):
 1. \<And>cdl_tcb z x2. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; (case ekheap s ptr of Some etcb \<Rightarrow> transform_tcb (machine_state s) ptr x2 etcb) = Tcb cdl_tcb; z = TCB x2; \<exists>etcb. ekheap s ptr = Some etcb\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 2. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (2 subgoals):
 1. \<And>cdl_tcb x2 etcb. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; transform_tcb (machine_state s) ptr x2 etcb = Tcb cdl_tcb; ekheap s ptr = Some etcb\<rbrakk> \<Longrightarrow> (ptr, cdl_tcb_domain cdl_tcb) \<in> domains_of_state s
 2. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (2 subgoals):
 1. \<And>cdl_tcb x2 etcb. \<lbrakk>invs s; valid_list s; valid_sched s; d = cdl_tcb_domain cdl_tcb; ptr \<noteq> idle_thread s; transform_tcb (machine_state s) ptr x2 etcb = Tcb cdl_tcb; ekheap s ptr = Some etcb\<rbrakk> \<Longrightarrow> cdl_tcb_domain cdl_tcb = tcb_domain etcb
 2. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr = idle_thread_ptr; d = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr = idle_thread_ptr; d = default_domain; idle_thread s = idle_thread_ptr\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr = idle_thread_ptr; d = default_domain; idle_thread s = idle_thread_ptr; \<exists>etcb. ekheap s idle_thread_ptr = Some etcb \<and> tcb_domain etcb = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (1 subgoal):
 1. \<And>etcb. \<lbrakk>ptr = idle_thread_ptr; d = default_domain; idle_thread s = idle_thread_ptr; ekheap s idle_thread_ptr = Some etcb; tcb_domain etcb = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> domains_of_state s proof (prove)
goal (1 subgoal):
 1. \<And>etcb. \<lbrakk>ptr = idle_thread_ptr; d = default_domain; idle_thread s = idle_thread_ptr; tcb_domain etcb = default_domain\<rbrakk> \<Longrightarrow> default_domain = tcb_domain etcb proof (prove)
goal:
No subgoals! proof (state)
this:
(ptr, d) \<in> domains_of_state s

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
this:
(?ptr2, ?d2) \<in> cdl_domains_of_state (transform s) \<Longrightarrow> (?ptr2, ?d2) \<in> domains_of_state s

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
this:
(?ptr2, ?d2) \<in> cdl_domains_of_state (transform s) \<Longrightarrow> (?ptr2, ?d2) \<in> domains_of_state s

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
this:
(?ptr2, ?d2) \<in> cdl_domains_of_state (transform s) \<Longrightarrow> (?ptr2, ?d2) \<in> domains_of_state s

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
this:
(ptr, d) \<in> domains_of_state s

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (prove)
using this:
(ptr, d) \<in> domains_of_state s

goal (1 subgoal):
 1. (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr = idle_thread_ptr\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s)
 2. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr = idle_thread_ptr; idle_thread s = idle_thread_ptr\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s)
 2. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr = idle_thread_ptr; idle_thread s = idle_thread_ptr; \<exists>etcb. ekheap s idle_thread_ptr = Some etcb \<and> tcb_domain etcb = default_domain\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s)
 2. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>etcb. \<lbrakk>ekheap s idle_thread_ptr = Some etcb; d = default_domain; ptr = idle_thread_ptr; idle_thread s = idle_thread_ptr; tcb_domain etcb = default_domain\<rbrakk> \<Longrightarrow> (idle_thread_ptr, default_domain) \<in> cdl_domains_of_state (transform s)
 2. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr; \<exists>tcb. kheap s ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
using this:
einvs s

goal (2 subgoals):
 1. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr; \<exists>tcb. kheap s ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>etcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr; \<exists>tcb. kheap s ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>etcb tcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr; kheap s ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (ptr, tcb_domain etcb) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>etcb tcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> ptr \<noteq> idle_thread s
 2. \<And>etcb tcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr; cdl_objects (transform s) ptr = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op ptr (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) ptr tcb, cdl_tcb_has_fault = tcb_has_fault tcb, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> (ptr, tcb_domain etcb) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>etcb tcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr; idle_thread s = idle_thread_ptr\<rbrakk> \<Longrightarrow> ptr \<noteq> idle_thread s
 2. \<And>etcb tcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr; cdl_objects (transform s) ptr = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op ptr (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) ptr tcb, cdl_tcb_has_fault = tcb_has_fault tcb, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> (ptr, tcb_domain etcb) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>etcb tcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr; cdl_objects (transform s) ptr = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op ptr (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) ptr tcb, cdl_tcb_has_fault = tcb_has_fault tcb, cdl_tcb_domain = tcb_domain etcb\<rparr>)\<rbrakk> \<Longrightarrow> (ptr, tcb_domain etcb) \<in> cdl_domains_of_state (transform s) proof (prove)
goal (1 subgoal):
 1. \<And>etcb tcb. \<lbrakk>ekheap s ptr = Some etcb; d = tcb_domain etcb; ptr \<noteq> idle_thread_ptr\<rbrakk> \<Longrightarrow> tcb_domain etcb = cdl_tcb_domain \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op ptr (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) ptr tcb, cdl_tcb_has_fault = tcb_has_fault tcb, cdl_tcb_domain = tcb_domain etcb\<rparr> proof (prove)
goal:
No subgoals! proof (state)
this:
(ptr, d) \<in> cdl_domains_of_state (transform s)

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
this:
(?ptr2, ?d2) \<in> domains_of_state s \<Longrightarrow> (?ptr2, ?d2) \<in> cdl_domains_of_state (transform s)

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (state)
this:
(?ptr2, ?d2) \<in> domains_of_state s \<Longrightarrow> (?ptr2, ?d2) \<in> cdl_domains_of_state (transform s)

goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (prove)
goal (1 subgoal):
 1. cdl_domains_of_state (transform s) = domains_of_state s proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> cdl_domains_of_state (transform s)) = (x \<in> domains_of_state s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. ((a, b) \<in> cdl_domains_of_state (transform s)) = ((a, b) \<in> domains_of_state s) proof (prove)
goal:
No subgoals! proof (state)
this:
cdl_domains_of_state (transform s) = domains_of_state s

goal:
No subgoals!