theory Invariants_AI

lemma valid_ep_typ:
  assumes P: "\<And>p. \<lbrace>typ_at ATCB p\<rbrace> f \<lbrace>\<lambda>rv. typ_at ATCB p\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_ep ep s\<rbrace> f \<lbrace>\<lambda>rv s. valid_ep ep s\<rbrace>" apply (case_tac ep,
         simp_all add: valid_ep_def hoare_post_taut tcb_at_typ) apply (rule hoare_vcg_conj_lift [OF hoare_vcg_prop]) apply (rule hoare_vcg_conj_lift [OF _ hoare_vcg_prop]) apply (rule hoare_vcg_const_Ball_lift [OF P]) apply (rule hoare_vcg_conj_lift [OF hoare_vcg_prop]) apply (rule hoare_vcg_conj_lift [OF _ hoare_vcg_prop]) apply (rule hoare_vcg_const_Ball_lift [OF P]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ep ep\<rbrace> f \<lbrace>\<lambda>rv. valid_ep ep\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>\<lambda>s. x2 \<noteq> [] \<and> (\<forall>t\<in>set x2. typ_at ATCB t s) \<and> distinct x2\<rbrace> f \<lbrace>\<lambda>rv s. x2 \<noteq> [] \<and> (\<forall>t\<in>set x2. typ_at ATCB t s) \<and> distinct x2\<rbrace>
 2. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>\<lambda>s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> f \<lbrace>\<lambda>rv s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set x2. typ_at ATCB t s) \<and> distinct x2\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>t\<in>set x2. typ_at ATCB t s) \<and> distinct x2\<rbrace>
 2. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>\<lambda>s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> f \<lbrace>\<lambda>rv s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set x2. typ_at ATCB t s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>t\<in>set x2. typ_at ATCB t s\<rbrace>
 2. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>\<lambda>s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> f \<lbrace>\<lambda>rv s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>\<lambda>s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> f \<lbrace>\<lambda>rv s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>t\<in>set x3. typ_at ATCB t s) \<and> distinct x3\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>t\<in>set x3. typ_at ATCB t s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>t\<in>set x3. typ_at ATCB t s\<rbrace> proof (prove)
goal:
No subgoals!