kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAInvsPre

lemma get_pd_of_thread_reachable:
  "get_pd_of_thread (kheap s) (arch_state s) t \<noteq> arm_global_pd (arch_state s)
   \<Longrightarrow> (\<exists>\<rhd> get_pd_of_thread (kheap s) (arch_state s) t) s" by (auto simp: get_pd_of_thread_vs_lookup
          split: Structures_A.kernel_object.splits if_split_asm option.splits
                 cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_pd_of_thread (kheap s) (arch_state s) t \<noteq> arm_global_pd (arch_state s) \<Longrightarrow> \<exists>ref. (ref \<rhd> get_pd_of_thread (kheap s) (arch_state s) t) s
theory ArchAInvsPre

lemma user_mem_dom_cong:
  "kheap s = kheap s' \<Longrightarrow> dom (user_mem s) = dom (user_mem s')" by (simp add: user_mem_def in_user_frame_def dom_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s = kheap s' \<Longrightarrow> dom (user_mem s) = dom (user_mem s')
theory ArchAInvsPre

lemma device_mem_dom_cong:
  "kheap s = kheap s' \<Longrightarrow> dom (device_mem s) = dom (device_mem s')" by (simp add: device_mem_def in_device_frame_def dom_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s = kheap s' \<Longrightarrow> dom (device_mem s) = dom (device_mem s')
theory ArchAInvsPre

lemma device_frame_in_device_region:
  "\<lbrakk>in_device_frame p s; pspace_respects_device_region s\<rbrakk>
  \<Longrightarrow> device_state (machine_state s) p \<noteq> None" by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_device_frame p s; pspace_respects_device_region s\<rbrakk> \<Longrightarrow> device_state (machine_state s) p \<noteq> None
theory AInvs

lemma pred_tcb_at_upd_apply:
  "pred_tcb_at proj P t (s\<lparr>kheap := p'\<rparr>) =
  pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(t := p' t)\<rparr>)" by (simp add: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj P t (s\<lparr>kheap := p'\<rparr>) = pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(t := p' t)\<rparr>)
theory AInvs

lemma akernel_invs:
  "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace>
  (call_kernel e) :: (unit,unit) s_monad
  \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace>" unfolding call_kernel_def by (wpsimp wp: activate_invs simp: active_from_running)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> call_kernel e \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace>
theory AInvs

lemma akernel_invs_det_ext:
  "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace>
  (call_kernel e) :: (unit,det_ext) s_monad
  \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace>" unfolding call_kernel_def by (wpsimp wp: activate_invs simp: active_from_running)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> call_kernel e \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace>
theory AInvs

lemma kernel_entry_invs:
  "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace>
  (kernel_entry e us) :: (user_context,unit) s_monad
  \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace>" apply (simp add: kernel_entry_def) apply (wp akernel_invs thread_set_invs_trivial thread_set_ct_in_state
         do_machine_op_ct_in_state hoare_weak_lift_imp hoare_vcg_disj_lift
      | clarsimp simp add: tcb_cap_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> kernel_entry e us \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set us (tcb_arch tcb)\<rparr>) t;
y <- call_kernel e;
gets cur_thread >>= thread_get (arch_tcb_context_get \<circ> tcb_arch)
od \<lbrace>\<lambda>rv. invs and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal:
No subgoals!
theory AInvs

lemma dom_restrict_plus_eq:
  "a \<inter> b \<union> b = b" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<inter> b \<union> b = b
theory AInvs

lemma user_memory_update[wp]:
  "\<lbrace>\<lambda>s. P (device_region s) \<rbrace> do_machine_op (user_memory_update a)
   \<lbrace>\<lambda>rv s. P (device_region s)\<rbrace>" by (simp add: do_machine_op_def user_memory_update_def simpler_modify_def
                valid_def bind_def gets_def return_def get_def select_f_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (dom (device_state (machine_state s)))\<rbrace> do_machine_op (user_memory_update a) \<lbrace>\<lambda>rv s. P (dom (device_state (machine_state s)))\<rbrace>
theory Deterministic_AI

lemma and_assoc: "(A and (B and C)) = (A and B and C)"  (* FIXME: eliminate *)
   by (simp add: pred_conj_aci)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A and (B and C)) = (A and B and C) proof (prove)
goal (1 subgoal):
 1. (A and (B and C)) = (A and B and C)
theory Deterministic_AI

lemma next_childD:
  "\<lbrakk>next_child slot t = Some child; valid_list_2 t m\<rbrakk>
   \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot" apply(simp only: valid_list_2_def) apply(erule conjE) apply(erule_tac x=slot in allE) apply(clarsimp simp: next_child_def valid_list_2_def) apply(case_tac "t slot") apply(simp) apply(fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_child slot t = Some child; valid_list_2 t m\<rbrakk> \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_child slot t = Some child; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p))\<rbrakk> \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_child slot t = Some child; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p)\<rbrakk> \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_child slot t = Some child; \<forall>p. distinct (t p); set (t slot) = {c. m c = Some slot}\<rbrakk> \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = Some child; \<forall>a b. distinct (t (a, b)); set (t slot) = {c. m c = Some slot}\<rbrakk> \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = Some child; \<forall>a b. distinct (t (a, b)); set (t slot) = {c. m c = Some slot}; t slot = []\<rbrakk> \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot
 2. \<And>a list. \<lbrakk>(case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = Some child; \<forall>a b. distinct (t (a, b)); set (t slot) = {c. m c = Some slot}; t slot = a # list\<rbrakk> \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>(case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = Some child; \<forall>a b. distinct (t (a, b)); set (t slot) = {c. m c = Some slot}; t slot = a # list\<rbrakk> \<Longrightarrow> (\<exists>xs. t slot = child # xs) \<and> m child = Some slot proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_child_NoneD:
  notes split_paired_All[simp del]
  shows "next_child slot t = None \<Longrightarrow> t slot = []" apply(simp add: next_child_def) apply(case_tac "t slot") apply(simp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_child slot t = None \<Longrightarrow> t slot = [] proof (prove)
goal (1 subgoal):
 1. (case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None \<Longrightarrow> t slot = [] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None; t slot = []\<rbrakk> \<Longrightarrow> t slot = []
 2. \<And>a list. \<lbrakk>(case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None; t slot = a # list\<rbrakk> \<Longrightarrow> t slot = [] proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>(case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None; t slot = a # list\<rbrakk> \<Longrightarrow> t slot = [] proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_child_None_empty_desc:
  notes split_paired_All[simp del]
  shows "valid_list_2 t m
    \<Longrightarrow> (next_child slot t = None) = (descendants_of slot m = {})" apply(simp add: valid_list_2_def) apply(erule conjE) apply(erule_tac x=slot in allE) apply(clarsimp simp: next_child_def) apply(case_tac "t slot") apply(simp add: no_children_empty_desc) apply(fastforce simp: descendants_of_def cdt_parent_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> (next_child slot t = None) = (descendants_of slot m = {}) proof (prove)
goal (1 subgoal):
 1. (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)) \<Longrightarrow> (next_child slot t = None) = (descendants_of slot m = {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p)\<rbrakk> \<Longrightarrow> (next_child slot t = None) = (descendants_of slot m = {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. distinct (t p); set (t slot) = {c. m c = Some slot}\<rbrakk> \<Longrightarrow> (next_child slot t = None) = (descendants_of slot m = {}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. distinct (t p); set (t slot) = {c. m c = Some slot}\<rbrakk> \<Longrightarrow> ((case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None) = (descendants_of slot m = {}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>p. distinct (t p); set (t slot) = {c. m c = Some slot}; t slot = []\<rbrakk> \<Longrightarrow> ((case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None) = (descendants_of slot m = {})
 2. \<And>a list. \<lbrakk>\<forall>p. distinct (t p); set (t slot) = {c. m c = Some slot}; t slot = a # list\<rbrakk> \<Longrightarrow> ((case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None) = (descendants_of slot m = {}) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<forall>p. distinct (t p); set (t slot) = {c. m c = Some slot}; t slot = a # list\<rbrakk> \<Longrightarrow> ((case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = None) = (descendants_of slot m = {}) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_sibD:
  "next_sib slot t m = Some child
   \<Longrightarrow> (\<exists>p. m slot = Some p \<and> after_in_list (t p) slot = Some child)" apply(clarsimp simp: next_sib_def) apply(case_tac "m slot") apply(simp) apply(clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_sib slot t m = Some child \<Longrightarrow> \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = Some child proof (prove)
goal (1 subgoal):
 1. (case m slot of None \<Rightarrow> None | Some p \<Rightarrow> after_in_list (t p) slot) = Some child \<Longrightarrow> \<exists>a b. m slot = Some (a, b) \<and> after_in_list (t (a, b)) slot = Some child proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(case m slot of None \<Rightarrow> None | Some p \<Rightarrow> after_in_list (t p) slot) = Some child; m slot = None\<rbrakk> \<Longrightarrow> \<exists>a b. m slot = Some (a, b) \<and> after_in_list (t (a, b)) slot = Some child
 2. \<And>a. \<lbrakk>(case m slot of None \<Rightarrow> None | Some p \<Rightarrow> after_in_list (t p) slot) = Some child; m slot = Some a\<rbrakk> \<Longrightarrow> \<exists>a b. m slot = Some (a, b) \<and> after_in_list (t (a, b)) slot = Some child proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>(case m slot of None \<Rightarrow> None | Some p \<Rightarrow> after_in_list (t p) slot) = Some child; m slot = Some a\<rbrakk> \<Longrightarrow> \<exists>a b. m slot = Some (a, b) \<and> after_in_list (t (a, b)) slot = Some child proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma desc_not_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "valid_mdb s \<Longrightarrow> slot \<notin> descendants_of slot (cdt s)" apply(fastforce simp: valid_mdb_def no_mloop_def descendants_of_def cdt_parent_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> slot \<notin> descendants_of slot (cdt s) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_childI:
  "t slot = child # xs
  \<Longrightarrow> next_child slot t = Some child" by (simp add: next_child_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t slot = child # xs \<Longrightarrow> next_child slot t = Some child
theory Deterministic_AI

lemma next_childI':
  "\<lbrakk>t slot = child # xs; x = Some child\<rbrakk>
  \<Longrightarrow> next_child slot t = x" by (simp add: next_child_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t slot = child # xs; x = Some child\<rbrakk> \<Longrightarrow> next_child slot t = x
theory Deterministic_AI

lemma next_sibI:
  "\<lbrakk>m slot = Some p; after_in_list (t p) slot = Some sib\<rbrakk>
  \<Longrightarrow> next_sib slot t m = Some sib" by (simp add: next_sib_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some p; after_in_list (t p) slot = Some sib\<rbrakk> \<Longrightarrow> next_sib slot t m = Some sib
theory Deterministic_AI

lemma next_sibI':
  "\<lbrakk>m slot = Some p; after_in_list (t p) slot = Some sib; x = Some sib\<rbrakk>
  \<Longrightarrow> next_sib slot t m = x" by (simp add: next_sib_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = Some p; after_in_list (t p) slot = Some sib; x = Some sib\<rbrakk> \<Longrightarrow> next_sib slot t m = x
theory Deterministic_AI

lemma next_child_NoneI:
  "t slot = [] \<Longrightarrow> next_child slot t = None" by (simp add: next_child_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t slot = [] \<Longrightarrow> next_child slot t = None
theory Deterministic_AI

lemma next_sib_NoneI:
  "m slot = None \<or> (m slot = Some p \<and> after_in_list (t p) slot = None) \<Longrightarrow> next_sib slot t m = None" by (fastforce simp: next_sib_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m slot = None \<or> m slot = Some p \<and> after_in_list (t p) slot = None \<Longrightarrow> next_sib slot t m = None
theory Deterministic_AI

lemma not_child_not_sib:
  "\<lbrakk>m slot = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> next_sib p t m \<noteq> Some slot" apply(simp add: next_sib_def) apply(case_tac "m p") apply(simp) apply(simp) apply(rule notI) apply(simp only: valid_list_2_def) apply(erule conjE) apply(erule_tac x=a in allE) apply(fastforce dest: after_in_list_in_list) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> next_sib p t m \<noteq> Some slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m slot = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m slot = None; valid_list_2 t m; m p = None\<rbrakk> \<Longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some slot
 2. \<And>a. \<lbrakk>m slot = None; valid_list_2 t m; m p = Some a\<rbrakk> \<Longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some slot proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m slot = None; valid_list_2 t m; m p = Some a\<rbrakk> \<Longrightarrow> (case m p of None \<Rightarrow> None | Some pa \<Rightarrow> after_in_list (t pa) p) \<noteq> Some slot proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m slot = None; valid_list_2 t m; m p = Some a\<rbrakk> \<Longrightarrow> after_in_list (t a) p \<noteq> Some slot proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m slot = None; valid_list_2 t m; m p = Some a; after_in_list (t a) p = Some slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m slot = None; (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); m p = Some a; after_in_list (t a) p = Some slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m slot = None; m p = Some a; after_in_list (t a) p = Some slot; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>m slot = None; m p = Some a; after_in_list (t a) p = Some slot; \<forall>p. distinct (t p); set (t a) = {c. m c = Some a}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma descendants_trans:
  "\<lbrakk>a \<in> descendants_of b m; b \<in> descendants_of c m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m" by (simp add: descendants_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> descendants_of b m; b \<in> descendants_of c m\<rbrakk> \<Longrightarrow> a \<in> descendants_of c m
theory Deterministic_AI

lemma cdt_power:
  "\<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); (p, f 0) \<in> {(p, c). m c = Some p} ^^ n\<rbrakk>
    \<Longrightarrow> p = f n" apply(induct n arbitrary: p) apply(simp) apply (metis (lifting, full_types) mem_Collect_eq option.inject prod.simps(2) relpow_Suc_D2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); (p, f 0) \<in> {(p, c). m c = Some p} ^^ n\<rbrakk> \<Longrightarrow> p = f n proof (prove)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); (p, f 0) \<in> {(p, c). m c = Some p} ^^ 0\<rbrakk> \<Longrightarrow> p = f 0
 2. \<And>n p. \<lbrakk>\<And>p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); (p, f 0) \<in> {(p, c). m c = Some p} ^^ n\<rbrakk> \<Longrightarrow> p = f n; \<forall>i. m (f i) = Some (f (Suc i)); (p, f 0) \<in> {(p, c). m c = Some p} ^^ Suc n\<rbrakk> \<Longrightarrow> p = f (Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n p. \<lbrakk>\<And>p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); (p, f 0) \<in> {(p, c). m c = Some p} ^^ n\<rbrakk> \<Longrightarrow> p = f n; \<forall>i. m (f i) = Some (f (Suc i)); (p, f 0) \<in> {(p, c). m c = Some p} ^^ Suc n\<rbrakk> \<Longrightarrow> p = f (Suc n) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma cdt_induct:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m\<rbrakk>
    \<Longrightarrow> P slot" apply(induct_tac rule: wf_induct[where r="cdt_parent_rel m"]) apply(simp add: wf_cdt_parent_rel) apply(simp add: cdt_parent_defs) apply(case_tac "m x") apply(simp) apply(erule_tac x=a in allE) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m\<rbrakk> \<Longrightarrow> P slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m\<rbrakk> \<Longrightarrow> wf (cdt_parent_rel m)
 2. \<And>x. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m; \<forall>y. m \<Turnstile> y \<leadsto> x \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m; \<forall>y. m \<Turnstile> y \<leadsto> x \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m; \<forall>y. m x = Some y \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m; \<forall>y. m x = Some y \<longrightarrow> P y; m x = None\<rbrakk> \<Longrightarrow> P x
 2. \<And>x a. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m; \<forall>y. m x = Some y \<longrightarrow> P y; m x = Some a\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m; \<forall>y. m x = Some y \<longrightarrow> P y; m x = Some a\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>\<And>x. m x = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>m x = Some y; P y\<rbrakk> \<Longrightarrow> P x; finite_depth m; m x = Some a; m x = Some a \<longrightarrow> P a\<rbrakk> \<Longrightarrow> P x proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_not_child_domintros:
  "(\<And>x. \<lbrakk>next_sib slot t m = None; m slot = Some x\<rbrakk>
    \<Longrightarrow> next_not_child_dom (x, t, m))
      \<Longrightarrow> next_not_child_dom (slot, t, m)" apply(rule accpI) apply(erule next_not_child_rel.cases) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>next_sib slot t m = None; m slot = Some x\<rbrakk> \<Longrightarrow> next_not_child_dom (x, t, m)) \<Longrightarrow> next_not_child_dom (slot, t, m) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<And>x. \<lbrakk>next_sib slot t m = None; m slot = Some x\<rbrakk> \<Longrightarrow> next_not_child_dom (x, t, m); next_not_child_rel y (slot, t, m)\<rbrakk> \<Longrightarrow> next_not_child_dom y proof (prove)
goal (1 subgoal):
 1. \<And>y slota ta ma x2. \<lbrakk>\<And>x. \<lbrakk>next_sib slot t m = None; m slot = Some x\<rbrakk> \<Longrightarrow> next_not_child_dom (x, t, m); y = (x2, ta, ma); (slot, t, m) = (slota, ta, ma); next_sib slota ta ma = None; ma slota = Some x2\<rbrakk> \<Longrightarrow> next_not_child_dom y proof (prove)
goal:
No subgoals!