theory CSpace_R

lemma set_cap_not_quite_corres':
  assumes cr:
  "pspace_relations (ekheap (a)) (kheap s) (ksPSpace s')"
  "ekheap (s)      = ekheap (a)"
  "cur_thread s    = ksCurThread s'"
  "idle_thread s   = ksIdleThread s'"
  "machine_state s = ksMachineState s'"
  "work_units_completed s = ksWorkUnitsCompleted s'"
  "domain_index s  = ksDomScheduleIdx s'"
  "domain_list s   = ksDomSchedule s'"
  "cur_domain s    = ksCurDomain s'"
  "domain_time s   = ksDomainTime s'"
  "(x,t') \<in> fst (updateCap p' c' s')"
  "valid_objs s" "pspace_aligned s" "pspace_distinct s" "cte_at p s"
  "pspace_aligned' s'" "pspace_distinct' s'"
  "interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s')"
  "(arch_state s, ksArchState s') \<in> arch_state_relation"
  assumes c: "cap_relation c c'"
  assumes p: "p' = cte_map p"
  shows "\<exists>t. ((),t) \<in> fst (set_cap c p s) \<and>
             pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and>
             cdt t              = cdt s \<and>
             cdt_list t         = cdt_list (s) \<and>
             ekheap t           = ekheap (s) \<and>
             scheduler_action t = scheduler_action (s) \<and>
             ready_queues t     = ready_queues (s) \<and>
             is_original_cap t  = is_original_cap s \<and>
             interrupt_state_relation (interrupt_irq_node t) (interrupt_states t)
                              (ksInterruptState t') \<and>
             (arch_state t, ksArchState t') \<in> arch_state_relation \<and>
             cur_thread t    = ksCurThread t' \<and>
             idle_thread t   = ksIdleThread t' \<and>
             machine_state t = ksMachineState t' \<and>
             work_units_completed t = ksWorkUnitsCompleted t' \<and>
             domain_index t  = ksDomScheduleIdx t' \<and>
             domain_list t   = ksDomSchedule t' \<and>
             cur_domain t    = ksCurDomain t' \<and>
             domain_time t   = ksDomainTime t'" apply (rule set_cap_not_quite_corres) using cr apply (fastforce simp: c p pspace_relations_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>t. ((), t) \<in> fst (set_cap c p s) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace t') \<and> cdt t = cdt s \<and> cdt_list t = cdt_list s \<and> ekheap t = ekheap s \<and> scheduler_action t = scheduler_action s \<and> ready_queues t = ready_queues s \<and> is_original_cap t = is_original_cap s \<and> interrupt_state_relation (interrupt_irq_node t) (interrupt_states t) (ksInterruptState t') \<and> (arch_state t, ksArchState t') \<in> arch_state_relation \<and> cur_thread t = ksCurThread t' \<and> idle_thread t = ksIdleThread t' \<and> machine_state t = ksMachineState t' \<and> work_units_completed t = ksWorkUnitsCompleted t' \<and> domain_index t = ksDomScheduleIdx t' \<and> domain_list t = ksDomSchedule t' \<and> cur_domain t = ksCurDomain t' \<and> domain_time t = ksDomainTime t' proof (prove)
goal (20 subgoals):
 1. pspace_relations (ekheap s) (kheap s) (ksPSpace ?s')
 2. cur_thread s = ksCurThread ?s'
 3. idle_thread s = ksIdleThread ?s'
 4. machine_state s = ksMachineState ?s'
 5. work_units_completed s = ksWorkUnitsCompleted ?s'
 6. domain_index s = ksDomScheduleIdx ?s'
 7. domain_list s = ksDomSchedule ?s'
 8. cur_domain s = ksCurDomain ?s'
 9. domain_time s = ksDomainTime ?s'
 10. (?x, t') \<in> fst (updateCap ?p' ?c' ?s')
A total of 20 subgoals... proof (prove)
using this:
pspace_relations (ekheap a) (kheap s) (ksPSpace s')
ekheap s = ekheap a
cur_thread s = ksCurThread s'
idle_thread s = ksIdleThread s'
machine_state s = ksMachineState s'
work_units_completed s = ksWorkUnitsCompleted s'
domain_index s = ksDomScheduleIdx s'
domain_list s = ksDomSchedule s'
cur_domain s = ksCurDomain s'
domain_time s = ksDomainTime s'
(x, t') \<in> fst (updateCap p' c' s')
valid_objs s
pspace_aligned s
pspace_distinct s
cte_wp_at (\<lambda>_. True) p s
pspace_aligned' s'
pspace_distinct' s'
interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s')
(arch_state s, ksArchState s') \<in> arch_state_relation

goal (20 subgoals):
 1. pspace_relations (ekheap s) (kheap s) (ksPSpace ?s')
 2. cur_thread s = ksCurThread ?s'
 3. idle_thread s = ksIdleThread ?s'
 4. machine_state s = ksMachineState ?s'
 5. work_units_completed s = ksWorkUnitsCompleted ?s'
 6. domain_index s = ksDomScheduleIdx ?s'
 7. domain_list s = ksDomSchedule ?s'
 8. cur_domain s = ksCurDomain ?s'
 9. domain_time s = ksDomainTime ?s'
 10. (?x, t') \<in> fst (updateCap ?p' ?c' ?s')
A total of 20 subgoals... proof (prove)
goal:
No subgoals!