theory ArchADT_IF

lemma idle_globals_lift:
  assumes g: "\<And>st. \<lbrace>globals_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
  assumes i: "\<And>s. P s \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s"
  shows "\<lbrace>idle_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" apply (clarsimp simp: valid_def) apply (subgoal_tac "arm_global_pd (arch_state s) \<noteq> idle_thread s") apply (subst (asm) idle_equiv_as_globals_equiv,simp+) apply (frule use_valid[OF _ g]) apply simp+ apply (clarsimp simp: idle_equiv_def globals_equiv_def tcb_at_def2) apply (erule i) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>idle_equiv st and P\<rbrace> f \<lbrace>\<lambda>_. idle_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); idle_equiv st s; P s\<rbrakk> \<Longrightarrow> idle_equiv st b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); idle_equiv st s; P s; arm_global_pd (arch_state s) \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> idle_equiv st b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); idle_equiv st s; P s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); globals_equiv (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, kheap := (kheap st)(arm_global_pd (arch_state s) := kheap s (arm_global_pd (arch_state s))), cur_thread := cur_thread s\<rparr>) s; P s; arm_global_pd (arch_state s) \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> idle_equiv st b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); idle_equiv st s; P s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); globals_equiv (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, kheap := (kheap st)(arm_global_pd (arch_state s) := kheap s (arm_global_pd (arch_state s))), cur_thread := cur_thread s\<rparr>) s; P s; arm_global_pd (arch_state s) \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (globals_equiv (?st14 s a b) and P) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); globals_equiv (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, kheap := (kheap st)(arm_global_pd (arch_state s) := kheap s (arm_global_pd (arch_state s))), cur_thread := cur_thread s\<rparr>) s; P s; arm_global_pd (arch_state s) \<noteq> idle_thread s; globals_equiv (?st14 s a b) b\<rbrakk> \<Longrightarrow> idle_equiv st b
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); idle_equiv st s; P s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); globals_equiv (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, kheap := (kheap st)(arm_global_pd (arch_state s) := kheap s (arm_global_pd (arch_state s))), cur_thread := cur_thread s\<rparr>) s; P s; arm_global_pd (arch_state s) \<noteq> idle_thread s; globals_equiv (st\<lparr>arch_state := arch_state s, machine_state := machine_state s, kheap := (kheap st)(arm_global_pd (arch_state s) := kheap s (arm_global_pd (arch_state s))), cur_thread := cur_thread s\<rparr>) b\<rbrakk> \<Longrightarrow> idle_equiv st b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); idle_equiv st s; P s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); idle_equiv st s; P s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state s) \<noteq> idle_thread s proof (prove)
goal:
No subgoals!