kings-crown/FVELER_Isabelle huggingface dataset:
theory Deterministic_AI

lemma next_sib_antisym:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "next_sib x t m = Some y \<Longrightarrow> next_sib y t m \<noteq> Some x" apply (rule notI) apply (frule next_sib_same_parent[OF valid_list]) apply (elim exE conjE) apply (drule next_sibD)+ apply (elim exE conjE) apply (simp add: valid_list[simplified valid_list_2_def] distinct_after_in_list_antisym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_sib x t m = Some y \<Longrightarrow> next_sib y t m \<noteq> Some x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib x t m = Some y; next_sib y t m = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib x t m = Some y; next_sib y t m = Some x; \<exists>p. m x = Some p \<and> m y = Some p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>next_sib x t m = Some y; next_sib y t m = Some x; m x = Some p; m y = Some p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>m x = Some p; m y = Some p; \<exists>p. m x = Some p \<and> after_in_list (t p) x = Some y; \<exists>p. m y = Some p \<and> after_in_list (t p) y = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p pa pb. \<lbrakk>m x = Some p; m y = Some p; m x = Some pa; after_in_list (t pa) x = Some y; m y = Some pb; after_in_list (t pb) y = Some x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma optionD: "x \<noteq> Some y \<Longrightarrow> x = None \<or> (\<exists>z. x = Some z \<and> z \<noteq> y)" by (case_tac "x"; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> Some y \<Longrightarrow> x = None \<or> (\<exists>z. x = Some z \<and> z \<noteq> y)
theory Deterministic_AI

lemma t_distinct: "distinct (t x)" by (simp add: valid_list[simplified valid_list_2_def])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (t x)
theory Deterministic_AI

lemma t_some[simp]: "set (t x) = {c. m c = Some x}" by (simp add: valid_list[simplified valid_list_2_def])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (t x) = {c. m c = Some x}
theory Deterministic_AI

lemma next_sibD':
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "next_sib slot t m = Some child \<Longrightarrow>
         \<exists>p. m slot = Some p \<and> m child = Some p \<and> after_in_list (t p) slot = Some child" apply (frule next_sib_same_parent[OF valid_list]) apply (drule next_sibD) 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> m child = Some p \<and> after_in_list (t p) slot = Some child proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot t m = Some child; \<exists>p. m slot = Some p \<and> m child = Some p\<rbrakk> \<Longrightarrow> \<exists>p. m slot = Some p \<and> m child = Some p \<and> after_in_list (t p) slot = Some child proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>p. m slot = Some p \<and> m child = Some p; \<exists>p. m slot = Some p \<and> after_in_list (t p) slot = Some child\<rbrakk> \<Longrightarrow> \<exists>p. m slot = Some p \<and> m child = Some p \<and> after_in_list (t p) slot = Some child proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma t'_empty:
  "(t' src = []) = (t dest = [])"
  "(t' dest = []) = (t src = [])"
  "p\<noteq>src \<and> p\<noteq>dest \<Longrightarrow> (t' p = []) = (t p = [])" by(fastforce simp: n_def n'_def t''_def t'_def list_swap_def
              split: option.splits split: if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (t' src = []) = (t dest = []) &&& (t' dest = []) = (t src = []) &&& (p \<noteq> src \<and> p \<noteq> dest \<Longrightarrow> (t' p = []) = (t p = []))
theory Deterministic_AI

lemma cap_delete_one_valid_list[wp]: "\<lbrace>valid_list\<rbrace> cap_delete_one a \<lbrace>\<lambda>_.valid_list\<rbrace>" unfolding cap_delete_one_def by (wpsimp simp: unless_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> cap_delete_one a \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do cap <- get_cap a;
unless (cap = NullCap) $ do final <- is_final_cap cap;
fast_finalise cap final;
empty_slot a NullCap
od
od \<lbrace>\<lambda>_. valid_list\<rbrace>
theory Deterministic_AI

lemma reply_cancel_ipc_valid_list[wp]: "\<lbrace>valid_list\<rbrace> reply_cancel_ipc a \<lbrace>\<lambda>_. valid_list\<rbrace>" unfolding reply_cancel_ipc_def by (wp hoare_drop_imps thread_set_mdb | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> reply_cancel_ipc a \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do thread_set (tcb_fault_update (\<lambda>_. None)) a;
cap <- get_cap (a, tcb_cnode_index 2);
descs <- gets (descendants_of (a, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) $ do assert (\<exists>cslot_ptr. descs = {cslot_ptr});
select descs >>= cap_delete_one
od
od \<lbrace>\<lambda>_. valid_list\<rbrace>
theory Deterministic_AI

lemma preemption_point_inv':
  "\<lbrakk>irq_state_independent_A P; \<And>f s. P (work_units_completed_update f s) = P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace>" apply (intro impI conjI | simp add: preemption_point_def o_def
       | wp hoare_post_imp[OF _ getActiveIRQ_wp] OR_choiceE_weak_wp
       | wpc | simp add: update_work_units_def reset_work_units_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_state_independent_A P; \<And>f s. P (work_units_completed_update f s) = P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> preemption_point \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma irq_state_independent_A_valid_list[simp]: "irq_state_independent_A valid_list" by (simp add: irq_state_independent_A_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_independent_A valid_list
theory Deterministic_AI

lemma cap_revoke_valid_list[wp]:"\<lbrace>valid_list\<rbrace> cap_revoke a \<lbrace>\<lambda>_. valid_list\<rbrace>" apply (rule cap_revoke_preservation2) apply (wp preemption_point_inv'|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> cap_revoke a \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrace>valid_list\<rbrace> cap_delete p \<lbrace>\<lambda>_. valid_list\<rbrace>
 2. \<And>s. \<lbrace>valid_list\<rbrace> preemption_point \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma invoke_cnode_valid_list[wp]:
  "\<lbrace>valid_list\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_.valid_list\<rbrace>" apply (rule hoare_pre) apply (wp crunch_wps cap_move_src_slot_Null hoare_drop_imps hoare_vcg_all_lift | wpc | simp add: invoke_cnode_def crunch_simps split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> invoke_cnode ci \<lbrace>\<lambda>_. valid_list\<rbrace>
 2. \<And>s. valid_list s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma delete_objects_valid_list[wp]: "\<lbrace>valid_list\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_.valid_list\<rbrace>" unfolding delete_objects_def apply (wp | simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do do_machine_op (freeMemory ptr bits);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma retype_region_ext_valid_list_ext[wp]: "\<lbrace>valid_list\<rbrace> retype_region_ext a b \<lbrace>\<lambda>_.valid_list\<rbrace>" by (wpsimp simp: retype_region_ext_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> retype_region_ext a b \<lbrace>\<lambda>_. valid_list\<rbrace>
theory Deterministic_AI

lemma handle_event_valid_list[wp]:
  "\<lbrace>valid_list\<rbrace> handle_event e \<lbrace>\<lambda>_.valid_list\<rbrace>" by (case_tac e; wpsimp wp: hoare_drop_imps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> handle_event e \<lbrace>\<lambda>_. valid_list\<rbrace>
theory Deterministic_AI

lemma (in mdb_move_abs') dest_empty_list:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "valid_list_2 t m \<Longrightarrow> t dest = []" apply (insert dest_desc) apply (subgoal_tac "set (t dest) = {}") apply simp apply (simp add: valid_list_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> t dest = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; descendants_of dest m = {}\<rbrakk> \<Longrightarrow> t dest = [] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; descendants_of dest m = {}; set (t dest) = {}\<rbrakk> \<Longrightarrow> t dest = []
 2. \<lbrakk>valid_list_2 t m; descendants_of dest m = {}\<rbrakk> \<Longrightarrow> set (t dest) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; descendants_of dest m = {}\<rbrakk> \<Longrightarrow> set (t dest) = {} proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma update_cdt_list_bind: "do y \<leftarrow> (update_cdt_list f); update_cdt_list f' od =
       update_cdt_list (\<lambda>s. f' (f s))" apply (simp add: bind_def update_cdt_list_def gets_def
                   return_def get_def set_cdt_list_def
                   put_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do y <- update_cdt_list f;
update_cdt_list f'
od = update_cdt_list (\<lambda>s. f' (f s)) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma update_list_eq: "(f (cdt_list e)) = (f' (cdt_list e)) \<Longrightarrow>
        update_cdt_list f e = update_cdt_list f' e" apply (simp add: update_cdt_list_def gets_def
                   get_def set_cdt_list_def put_def
                   bind_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (cdt_list e) = f' (cdt_list e) \<Longrightarrow> update_cdt_list f e = update_cdt_list f' e proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma (in mdb_insert_abs) create_cap_ext_det_def2:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
 "valid_list_2 (cdt_list e) m \<Longrightarrow> dest_p = (m dest) \<Longrightarrow>
       create_cap_ext untyped dest dest_p e = (
    update_cdt_list (\<lambda>list. list (untyped := [dest] @ list untyped))) e" apply (simp add: create_cap_ext_def update_cdt_list_bind) apply (rule update_list_eq) apply (insert dest neq) apply (case_tac "m src") apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; dest_p = m dest\<rbrakk> \<Longrightarrow> create_cap_ext untyped dest dest_p e = update_cdt_list (\<lambda>list. list(untyped := [dest] @ list untyped)) e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; dest_p = m dest\<rbrakk> \<Longrightarrow> update_cdt_list (\<lambda>s. (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest))(untyped := dest # (case m dest of None \<Rightarrow> s | Some p \<Rightarrow> s(p := list_remove (s p) dest)) untyped)) e = update_cdt_list (\<lambda>list. list(untyped := dest # list untyped)) e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; dest_p = m dest\<rbrakk> \<Longrightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(untyped := dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) untyped) = (cdt_list e)(untyped := dest # cdt_list e untyped) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; dest_p = m dest; m dest = None; src \<noteq> dest\<rbrakk> \<Longrightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(untyped := dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) untyped) = (cdt_list e)(untyped := dest # cdt_list e untyped) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 (cdt_list e) m; dest_p = m dest; m dest = None; src \<noteq> dest; m src = None\<rbrakk> \<Longrightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(untyped := dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) untyped) = (cdt_list e)(untyped := dest # cdt_list e untyped)
 2. \<And>a. \<lbrakk>valid_list_2 (cdt_list e) m; dest_p = m dest; m dest = None; src \<noteq> dest; m src = Some a\<rbrakk> \<Longrightarrow> (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest))(untyped := dest # (case m dest of None \<Rightarrow> cdt_list e | Some p \<Rightarrow> (cdt_list e)(p := list_remove (cdt_list e p) dest)) untyped) = (cdt_list e)(untyped := dest # cdt_list e untyped) proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_sib_2_domintros:
  "(\<And>x. \<lbrakk>slot \<in> descendants_of p (cdt s);
      next_slot slot (cdt_list s) (cdt s) = Some x;  cdt s x \<noteq> Some p\<rbrakk>
    \<Longrightarrow> next_sib_2_dom (x, p, s))
      \<Longrightarrow> next_sib_2_dom (slot, p, s)" apply(rule accpI) apply(erule next_sib_2_rel.cases) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some x; cdt s x \<noteq> Some p\<rbrakk> \<Longrightarrow> next_sib_2_dom (x, p, s)) \<Longrightarrow> next_sib_2_dom (slot, p, s) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<And>x. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some x; cdt s x \<noteq> Some p\<rbrakk> \<Longrightarrow> next_sib_2_dom (x, p, s); next_sib_2_rel y (slot, p, s)\<rbrakk> \<Longrightarrow> next_sib_2_dom y proof (prove)
goal (1 subgoal):
 1. \<And>y slota pa sa x2. \<lbrakk>\<And>x. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some x; cdt s x \<noteq> Some p\<rbrakk> \<Longrightarrow> next_sib_2_dom (x, p, s); y = (x2, pa, sa); (slot, p, s) = (slota, pa, sa); slota \<in> descendants_of pa (cdt sa); next_slot slota (cdt_list sa) (cdt sa) = Some x2; cdt sa x2 \<noteq> Some pa\<rbrakk> \<Longrightarrow> next_sib_2_dom y proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_sib_set_same_parent:
  "\<lbrakk>next \<in> next_sib_set slot t m; valid_list_2 t m\<rbrakk>
    \<Longrightarrow> \<exists>p. m slot = Some p \<and> m next = Some p" apply (simp add: next_sib_set_def) by (induct "next" slot rule: trancl.induct; fastforce dest: next_sib_same_parent)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next \<in> next_sib_set slot t m; valid_list_2 t m\<rbrakk> \<Longrightarrow> \<exists>p. m slot = Some p \<and> m next = Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(next, slot) \<in> {(next, p). next_sib p t m = Some next}\<^sup>+; valid_list_2 t m\<rbrakk> \<Longrightarrow> \<exists>a b. m slot = Some (a, b) \<and> m next = Some (a, b)
theory Deterministic_AI

lemma next_sib_set_eq_after_in_list_set:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "valid_list_2 t m \<Longrightarrow> next_sib_set x t m = (case m x of None \<Rightarrow> {}
    | Some q \<Rightarrow> {a. (a, x) \<in> {(next, p). after_in_list (t q) p = Some next}\<^sup>+})" apply(simp add: next_sib_set_eq_after_in_list_set_Some split: option.splits) apply(fastforce simp: next_sib_set_def next_sib_def split: option.splits dest: tranclD2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> next_sib_set x t m = (case m x of None \<Rightarrow> {} | Some q \<Rightarrow> {a. (a, x) \<in> {(next, p). after_in_list (t q) p = Some next}\<^sup>+}) proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> m x = None \<longrightarrow> next_sib_set x t m = {} proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma valid_list_distinct:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>valid_list_2 t m; m x = Some p\<rbrakk> \<Longrightarrow> distinct (t p)" by (simp add:valid_list_2_def)

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

lemma next_sib_set_not_self:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "valid_list_2 t m \<Longrightarrow> x \<notin> next_sib_set x t m" apply(simp add: next_sib_set_eq_after_in_list_set valid_list_distinct after_in_list_list_set[symmetric] split: option.splits) apply(intro allI impI) apply(frule_tac p="the (m x)" in list_eq_after_in_list) apply(simp) apply(clarsimp simp add: valid_list_2_def) apply(erule_tac x="the (m x)" in allE)+ apply(drule_tac x="t x" and f=distinct for x in arg_cong) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> x \<notin> next_sib_set x t m proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m \<Longrightarrow> \<forall>x2. m x = Some x2 \<longrightarrow> x \<notin> set (after_in_list_list (t x2) x) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>valid_list_2 t m; m x = Some x2\<rbrakk> \<Longrightarrow> x \<notin> set (after_in_list_list (t x2) x) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>valid_list_2 t m; m x = Some x2\<rbrakk> \<Longrightarrow> m (?x10 x2) = Some (the (m x))
 2. \<And>x2. \<lbrakk>valid_list_2 t m; m x = Some x2; \<exists>list. t (the (m x)) = list @ ?x10 x2 # after_in_list_list (t (the (m x))) (?x10 x2)\<rbrakk> \<Longrightarrow> x \<notin> set (after_in_list_list (t x2) x) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>valid_list_2 t m; m x = Some x2; \<exists>list. t (the (m x)) = list @ x # after_in_list_list (t (the (m x))) x\<rbrakk> \<Longrightarrow> x \<notin> set (after_in_list_list (t x2) x) proof (prove)
goal (1 subgoal):
 1. \<And>a b list. \<lbrakk>m x = Some (a, b); t (a, b) = list @ x # after_in_list_list (t (a, b)) x; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); x \<in> set (after_in_list_list (t (a, b)) x)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b list. \<lbrakk>m x = Some (a, b); t (a, b) = list @ x # after_in_list_list (t (a, b)) x; x \<in> set (after_in_list_list (t (a, b)) x); set (t (the (m x))) = {c. m c = Some (the (m x))}; distinct (t (the (m x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b list. \<lbrakk>m x = Some (a, b); x \<in> set (after_in_list_list (t (a, b)) x); set (t (the (m x))) = {c. m c = Some (the (m x))}; distinct (t (the (m x))); distinct (t (a, b)) = distinct (list @ x # after_in_list_list (t (a, b)) x)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_slot_induct:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "\<lbrakk>\<And>x. next_slot x (cdt_list s) (cdt s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; P y\<rbrakk> \<Longrightarrow> P x;
    valid_mdb s; valid_list s\<rbrakk>
    \<Longrightarrow> P slot" apply(induct_tac rule: wf_induct[where r="{(next, p). next_slot p (cdt_list s) (cdt s) = Some next}"]) apply(simp add: wf_next_slot) apply(fastforce split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. next_slot x (cdt_list s) (cdt s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; P y\<rbrakk> \<Longrightarrow> P x; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> P slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. next_slot x (cdt_list s) (cdt s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; P y\<rbrakk> \<Longrightarrow> P x; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> wf {(next, p). next_slot p (cdt_list s) (cdt s) = Some next}
 2. \<And>x. \<lbrakk>\<And>x. next_slot x (cdt_list s) (cdt s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; P y\<rbrakk> \<Longrightarrow> P x; valid_mdb s; valid_list s; \<forall>y. (y, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next} \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. next_slot x (cdt_list s) (cdt s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>next_slot x (cdt_list s) (cdt s) = Some y; P y\<rbrakk> \<Longrightarrow> P x; valid_mdb s; valid_list s; \<forall>y. (y, x) \<in> {(next, p). next_slot p (cdt_list s) (cdt s) = Some next} \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_sib_2_termination:
  "\<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> next_sib_2_dom (slot, p, s)" apply(induct_tac slot rule: next_slot_induct[where s=s]) apply(fastforce intro: next_sib_2_domintros)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> next_sib_2_dom (slot, p, s) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>valid_mdb s; valid_list s; next_slot x (cdt_list s) (cdt s) = None\<rbrakk> \<Longrightarrow> next_sib_2_dom (x, p, s)
 2. \<And>x y. \<lbrakk>valid_mdb s; valid_list s; next_slot x (cdt_list s) (cdt s) = Some y; next_sib_2_dom (y, p, s)\<rbrakk> \<Longrightarrow> next_sib_2_dom (x, p, s)
 3. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> valid_mdb s
 4. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> valid_list s proof (prove)
goal:
No subgoals!