theory ADT_H

lemma ex1_sorted_cdt: "\<exists>!xs. set xs = {c. m c = Some p} \<and>
           psorted xs \<and>
           distinct xs" apply (rule psorted_set[OF finite_children]) apply (simp add: R_set_def) apply (intro impI conjI allI) apply (simp add: has_parent_cte_at[OF valid_mdb] m_def) apply (simp add: has_parent_cte_at[OF valid_mdb] m_def) apply (cut_tac s=s and s'=s' and x="(a,b)" in cdt_simple_rel, simp_all add: assms' rel) apply (simp add: m_def) apply (cut_tac s=s and s'=s' and x="(aa,ba)" in cdt_simple_rel, simp_all add: assms' rel) apply (rule_tac x="cte_map p" in exI) apply (simp add: m'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>!xs. set xs = {c. m c = Some p} \<and> psorted xs \<and> distinct xs proof (prove)
goal (1 subgoal):
 1. R_set {c. m c = Some p} proof (prove)
goal (1 subgoal):
 1. \<forall>a b. m (a, b) = Some p \<longrightarrow> (\<forall>aa ba. m (aa, ba) = Some p \<longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> cte_wp_at (\<lambda>_. True) (aa, ba) s \<and> (\<exists>p. m' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> m' \<turnstile> p \<rightarrow> cte_map (aa, ba))) proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. \<lbrakk>m (a, b) = Some p; m (aa, ba) = Some p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s
 2. \<And>a b aa ba. \<lbrakk>m (a, b) = Some p; m (aa, ba) = Some p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, ba) s
 3. \<And>a b aa ba. \<lbrakk>m (a, b) = Some p; m (aa, ba) = Some p\<rbrakk> \<Longrightarrow> \<exists>p. m' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> m' \<turnstile> p \<rightarrow> cte_map (aa, ba) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>m (a, b) = Some p; m (aa, ba) = Some p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, ba) s
 2. \<And>a b aa ba. \<lbrakk>m (a, b) = Some p; m (aa, ba) = Some p\<rbrakk> \<Longrightarrow> \<exists>p. m' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> m' \<turnstile> p \<rightarrow> cte_map (aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>m (a, b) = Some p; m (aa, ba) = Some p\<rbrakk> \<Longrightarrow> \<exists>p. m' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> m' \<turnstile> p \<rightarrow> cte_map (aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>m (a, b) = Some p; m (aa, ba) = Some p; case cdt s (a, b) of None \<Rightarrow> (\<exists>y. caps_of_state s (a, b) = Some y) \<longrightarrow> (\<forall>q. \<not> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b)) | Some p \<Rightarrow> ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map p = q)\<rbrakk> \<Longrightarrow> \<exists>p. m' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> m' \<turnstile> p \<rightarrow> cte_map (aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cdt s (a, b) = Some p; cdt s (aa, ba) = Some p; ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map p = q)\<rbrakk> \<Longrightarrow> \<exists>p. m' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> m' \<turnstile> p \<rightarrow> cte_map (aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cdt s (a, b) = Some p; cdt s (aa, ba) = Some p; ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map p = q); ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map (aa, ba) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (aa, ba) \<longrightarrow> cte_map p = q)\<rbrakk> \<Longrightarrow> \<exists>p. m' \<turnstile> p \<rightarrow> cte_map (a, b) \<and> m' \<turnstile> p \<rightarrow> cte_map (aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cdt s (a, b) = Some p; cdt s (aa, ba) = Some p; ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map (a, b) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (a, b) \<longrightarrow> cte_map p = q); ctes_of s' \<turnstile> cte_map p \<rightarrow> cte_map (aa, ba) \<and> (\<forall>q. ctes_of s' \<turnstile> cte_map p \<rightarrow> q \<and> ctes_of s' \<turnstile> q \<rightarrow> cte_map (aa, ba) \<longrightarrow> cte_map p = q)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map p \<rightarrow> cte_map (a, b) \<and> m' \<turnstile> cte_map p \<rightarrow> cte_map (aa, ba) proof (prove)
goal:
No subgoals!