theory KHeap_AI

lemma set_simple_ko_hyp_refs_of[wp]:
 "set_simple_ko f ep val \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>" apply (set_simple_ko_method wp_thm: set_object_wp_strong) apply (rule conjI; clarsimp elim!: rsubst[where P=P]) apply (subst state_hyp_refs_of_ep_update[of ep, symmetric]) apply (clarsimp simp: obj_at_def) apply (simp add: fun_upd_def) apply (subst state_hyp_refs_of_ntfn_update[of ep, symmetric]) apply (clarsimp simp: obj_at_def) apply (simp add: fun_upd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> set_simple_ko f ep val \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_hyp_refs_of s) \<Longrightarrow> (\<forall>x3. f val = Endpoint x3 \<longrightarrow> (\<forall>x3a. (\<exists>!y. f y = Endpoint x3a) \<longrightarrow> kheap s ep = Some (Endpoint x3a) \<longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint x3)\<rparr>)))) \<and> (\<forall>x4. f val = Notification x4 \<longrightarrow> (\<forall>x4a. (\<exists>!y. f y = Notification x4a) \<longrightarrow> kheap s ep = Some (Notification x4a) \<longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification x4)\<rparr>)))) proof (prove)
goal (2 subgoals):
 1. \<And>s x3 x3a y. \<lbrakk>f val = Endpoint x3; f y = Endpoint x3a; \<forall>y y'. f y = Endpoint x3a \<and> f y' = Endpoint x3a \<longrightarrow> y = y'; kheap s ep = Some (Endpoint x3a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of s = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint x3)\<rparr>)
 2. \<And>s x4 x4a y. \<lbrakk>f val = Notification x4; f y = Notification x4a; \<forall>y y'. f y = Notification x4a \<and> f y' = Notification x4a \<longrightarrow> y = y'; kheap s ep = Some (Notification x4a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of s = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification x4)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x3 x3a y. \<lbrakk>f val = Endpoint x3; f y = Endpoint x3a; \<forall>y y'. f y = Endpoint x3a \<and> f y' = Endpoint x3a \<longrightarrow> y = y'; kheap s ep = Some (Endpoint x3a)\<rbrakk> \<Longrightarrow> typ_at AEndpoint ep s
 2. \<And>s x3 x3a y. \<lbrakk>f val = Endpoint x3; f y = Endpoint x3a; \<forall>y y'. f y = Endpoint x3a \<and> f y' = Endpoint x3a \<longrightarrow> y = y'; kheap s ep = Some (Endpoint x3a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint (?val114 s x3 x3a y))\<rparr>) = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint x3)\<rparr>)
 3. \<And>s x4 x4a y. \<lbrakk>f val = Notification x4; f y = Notification x4a; \<forall>y y'. f y = Notification x4a \<and> f y' = Notification x4a \<longrightarrow> y = y'; kheap s ep = Some (Notification x4a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of s = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification x4)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x3 x3a y. \<lbrakk>f val = Endpoint x3; f y = Endpoint x3a; \<forall>y y'. f y = Endpoint x3a \<and> f y' = Endpoint x3a \<longrightarrow> y = y'; kheap s ep = Some (Endpoint x3a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint (?val114 s x3 x3a y))\<rparr>) = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint x3)\<rparr>)
 2. \<And>s x4 x4a y. \<lbrakk>f val = Notification x4; f y = Notification x4a; \<forall>y y'. f y = Notification x4a \<and> f y' = Notification x4a \<longrightarrow> y = y'; kheap s ep = Some (Notification x4a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of s = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification x4)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x4 x4a y. \<lbrakk>f val = Notification x4; f y = Notification x4a; \<forall>y y'. f y = Notification x4a \<and> f y' = Notification x4a \<longrightarrow> y = y'; kheap s ep = Some (Notification x4a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of s = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification x4)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x4 x4a y. \<lbrakk>f val = Notification x4; f y = Notification x4a; \<forall>y y'. f y = Notification x4a \<and> f y' = Notification x4a \<longrightarrow> y = y'; kheap s ep = Some (Notification x4a)\<rbrakk> \<Longrightarrow> typ_at ANTFN ep s
 2. \<And>s x4 x4a y. \<lbrakk>f val = Notification x4; f y = Notification x4a; \<forall>y y'. f y = Notification x4a \<and> f y' = Notification x4a \<longrightarrow> y = y'; kheap s ep = Some (Notification x4a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification (?val117 s x4 x4a y))\<rparr>) = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification x4)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x4 x4a y. \<lbrakk>f val = Notification x4; f y = Notification x4a; \<forall>y y'. f y = Notification x4a \<and> f y' = Notification x4a \<longrightarrow> y = y'; kheap s ep = Some (Notification x4a)\<rbrakk> \<Longrightarrow> state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification (?val117 s x4 x4a y))\<rparr>) = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification x4)\<rparr>) proof (prove)
goal:
No subgoals!