theory Example_Valid_StateH

lemma kh0H_dom_distinct':
  "length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> init_globals_frame"
  "length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> idle_tcb_ptr"
  "length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> High_tcb_ptr"
  "length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> Low_tcb_ptr"
  "length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> irq_cnode_ptr"
  "length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> ntfn_ptr"
  "length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> init_globals_frame"
  "length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> idle_tcb_ptr"
  "length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> High_tcb_ptr"
  "length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> Low_tcb_ptr"
  "length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> irq_cnode_ptr"
  "length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> ntfn_ptr"
  "length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> init_globals_frame"
  "length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> idle_tcb_ptr"
  "length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> High_tcb_ptr"
  "length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> Low_tcb_ptr"
  "length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> irq_cnode_ptr"
  "length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> ntfn_ptr"
  "Low_pd_ptr + (ucast (y::12 word) << 2) \<noteq> init_globals_frame"
  "Low_pd_ptr + (ucast (y::12 word) << 2) \<noteq> idle_tcb_ptr"
  "Low_pd_ptr + (ucast (y::12 word) << 2) \<noteq> High_tcb_ptr"
  "Low_pd_ptr + (ucast (y::12 word) << 2) \<noteq> Low_tcb_ptr"
  "Low_pd_ptr + (ucast (y::12 word) << 2) \<noteq> irq_cnode_ptr"
  "Low_pd_ptr + (ucast (y::12 word) << 2) \<noteq> ntfn_ptr"
  "High_pd_ptr + (ucast (y::12 word) << 2) \<noteq> init_globals_frame"
  "High_pd_ptr + (ucast (y::12 word) << 2) \<noteq> idle_tcb_ptr"
  "High_pd_ptr + (ucast (y::12 word) << 2) \<noteq> High_tcb_ptr"
  "High_pd_ptr + (ucast (y::12 word) << 2) \<noteq> Low_tcb_ptr"
  "High_pd_ptr + (ucast (y::12 word) << 2) \<noteq> irq_cnode_ptr"
  "High_pd_ptr + (ucast (y::12 word) << 2) \<noteq> ntfn_ptr"
  "init_global_pd + (ucast (y::12 word) << 2) \<noteq> init_globals_frame"
  "init_global_pd + (ucast (y::12 word) << 2) \<noteq> idle_tcb_ptr"
  "init_global_pd + (ucast (y::12 word) << 2) \<noteq> High_tcb_ptr"
  "init_global_pd + (ucast (y::12 word) << 2) \<noteq> Low_tcb_ptr"
  "init_global_pd + (ucast (y::12 word) << 2) \<noteq> irq_cnode_ptr"
  "init_global_pd + (ucast (y::12 word) << 2) \<noteq> ntfn_ptr"
  "Low_pt_ptr + (ucast (z::8 word) << 2) \<noteq> init_globals_frame"
  "Low_pt_ptr + (ucast (z::8 word) << 2) \<noteq> idle_tcb_ptr"
  "Low_pt_ptr + (ucast (z::8 word) << 2) \<noteq> High_tcb_ptr"
  "Low_pt_ptr + (ucast (z::8 word) << 2) \<noteq> Low_tcb_ptr"
  "Low_pt_ptr + (ucast (z::8 word) << 2) \<noteq> irq_cnode_ptr"
  "Low_pt_ptr + (ucast (z::8 word) << 2) \<noteq> ntfn_ptr"
  "High_pt_ptr + (ucast (z::8 word) << 2) \<noteq> init_globals_frame"
  "High_pt_ptr + (ucast (z::8 word) << 2) \<noteq> idle_tcb_ptr"
  "High_pt_ptr + (ucast (z::8 word) << 2) \<noteq> High_tcb_ptr"
  "High_pt_ptr + (ucast (z::8 word) << 2) \<noteq> Low_tcb_ptr"
  "High_pt_ptr + (ucast (z::8 word) << 2) \<noteq> irq_cnode_ptr"
  "High_pt_ptr + (ucast (z::8 word) << 2) \<noteq> ntfn_ptr" apply (drule offs_in_range, fastforce simp: kh0H_dom_distinct)+ apply (cut_tac x=y in offs_in_range(1), fastforce simp: kh0H_dom_distinct)+ apply (cut_tac x=y in offs_in_range(2), fastforce simp: kh0H_dom_distinct)+ apply (cut_tac x=y in offs_in_range(3), fastforce simp: kh0H_dom_distinct)+ apply (cut_tac x=z in offs_in_range(4), fastforce simp: kh0H_dom_distinct)+ apply (cut_tac x=z in offs_in_range(5), fastforce simp: kh0H_dom_distinct)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((((length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> init_globals_frame) &&& (length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> idle_tcb_ptr) &&& (length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> High_tcb_ptr)) &&& (length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> Low_tcb_ptr) &&& (length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> irq_cnode_ptr) &&& (length x = 10 \<Longrightarrow> Silc_cnode_ptr + of_bl x * 0x10 \<noteq> ntfn_ptr)) &&& ((length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> init_globals_frame) &&& (length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> idle_tcb_ptr) &&& (length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> High_tcb_ptr)) &&& (length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> Low_tcb_ptr) &&& (length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> irq_cnode_ptr) &&& (length x = 10 \<Longrightarrow> Low_cnode_ptr + of_bl x * 0x10 \<noteq> ntfn_ptr)) &&& (((length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> init_globals_frame) &&& (length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> idle_tcb_ptr) &&& (length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> High_tcb_ptr)) &&& (length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> Low_tcb_ptr) &&& (length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> irq_cnode_ptr) &&& (length x = 10 \<Longrightarrow> High_cnode_ptr + of_bl x * 0x10 \<noteq> ntfn_ptr)) &&& (Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> init_globals_frame &&& Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> idle_tcb_ptr &&& Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> High_tcb_ptr) &&& Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> Low_tcb_ptr &&& Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> irq_cnode_ptr &&& Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> ntfn_ptr) &&& (((High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> init_globals_frame &&& High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> idle_tcb_ptr &&& High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> High_tcb_ptr) &&& High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> Low_tcb_ptr &&& High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> irq_cnode_ptr &&& High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> ntfn_ptr) &&& (init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> init_globals_frame &&& init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> idle_tcb_ptr &&& init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> High_tcb_ptr) &&& init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> Low_tcb_ptr &&& init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> irq_cnode_ptr &&& init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> ntfn_ptr) &&& ((Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> init_globals_frame &&& Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> idle_tcb_ptr &&& Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> High_tcb_ptr) &&& Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> Low_tcb_ptr &&& Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> irq_cnode_ptr &&& Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> ntfn_ptr) &&& (High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> init_globals_frame &&& High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> idle_tcb_ptr &&& High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> High_tcb_ptr) &&& High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> Low_tcb_ptr &&& High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> irq_cnode_ptr &&& High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> ntfn_ptr proof (prove)
goal (30 subgoals):
 1. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> init_globals_frame
 2. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> idle_tcb_ptr
 3. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> High_tcb_ptr
 4. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> Low_tcb_ptr
 5. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> irq_cnode_ptr
 6. Low_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> ntfn_ptr
 7. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> init_globals_frame
 8. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> idle_tcb_ptr
 9. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> High_tcb_ptr
 10. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> Low_tcb_ptr
A total of 30 subgoals... proof (prove)
goal (24 subgoals):
 1. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> init_globals_frame
 2. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> idle_tcb_ptr
 3. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> High_tcb_ptr
 4. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> Low_tcb_ptr
 5. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> irq_cnode_ptr
 6. High_pd_ptr + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> ntfn_ptr
 7. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> init_globals_frame
 8. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> idle_tcb_ptr
 9. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> High_tcb_ptr
 10. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> Low_tcb_ptr
A total of 24 subgoals... proof (prove)
goal (18 subgoals):
 1. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> init_globals_frame
 2. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> idle_tcb_ptr
 3. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> High_tcb_ptr
 4. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> Low_tcb_ptr
 5. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> irq_cnode_ptr
 6. init_global_pd + (UCAST(12 \<rightarrow> 32) y << 2) \<noteq> ntfn_ptr
 7. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> init_globals_frame
 8. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> idle_tcb_ptr
 9. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> High_tcb_ptr
 10. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> Low_tcb_ptr
A total of 18 subgoals... proof (prove)
goal (12 subgoals):
 1. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> init_globals_frame
 2. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> idle_tcb_ptr
 3. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> High_tcb_ptr
 4. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> Low_tcb_ptr
 5. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> irq_cnode_ptr
 6. Low_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> ntfn_ptr
 7. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> init_globals_frame
 8. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> idle_tcb_ptr
 9. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> High_tcb_ptr
 10. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> Low_tcb_ptr
A total of 12 subgoals... proof (prove)
goal (6 subgoals):
 1. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> init_globals_frame
 2. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> idle_tcb_ptr
 3. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> High_tcb_ptr
 4. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> Low_tcb_ptr
 5. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> irq_cnode_ptr
 6. High_pt_ptr + (UCAST(8 \<rightarrow> 32) z << 2) \<noteq> ntfn_ptr proof (prove)
goal:
No subgoals!