theory ADT_C

lemma inj_hwasidsI:
  "asid_map_pd_to_hwasids m = set_option \<circ> c \<Longrightarrow>
   inj_on (map_option snd \<circ> m) (dom m) \<Longrightarrow>
   inj_on (map_option fst \<circ> m) (dom m) \<Longrightarrow>
   inj_on c (dom c)" apply (clarsimp simp: asid_map_pd_to_hwasids_def inj_on_def) apply (clarsimp simp: fun_eq_iff set_eq_iff) apply (rename_tac x y z) apply (frule_tac x=x in spec, drule_tac x=z in spec) apply (drule_tac x=y in spec, drule_tac x=z in spec) apply (fastforce simp: ran_def dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid_map_pd_to_hwasids m = set_option \<circ> c; inj_on (map_option snd \<circ> m) (dom m); inj_on (map_option fst \<circ> m) (dom m)\<rbrakk> \<Longrightarrow> inj_on c (dom c) proof (prove)
goal (1 subgoal):
 1. \<And>x y ya. \<lbrakk>(\<lambda>pd. {hwasid. (hwasid, pd) \<in> ran m}) = set_option \<circ> c; \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option snd (m x) = map_option snd (m y) \<longrightarrow> x = y; \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option fst (m x) = map_option fst (m y) \<longrightarrow> x = y; c y = Some ya; c x = Some ya\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y ya. \<lbrakk>\<forall>x xa. ((xa, x) \<in> ran m) = (c x = Some xa); \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option snd (m x) = map_option snd (m y) \<longrightarrow> x = y; \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option fst (m x) = map_option fst (m y) \<longrightarrow> x = y; c y = Some ya; c x = Some ya\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>\<forall>x xa. ((xa, x) \<in> ran m) = (c x = Some xa); \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option snd (m x) = map_option snd (m y) \<longrightarrow> x = y; \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option fst (m x) = map_option fst (m y) \<longrightarrow> x = y; c y = Some z; c x = Some z\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>\<forall>x xa. ((xa, x) \<in> ran m) = (c x = Some xa); \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option snd (m x) = map_option snd (m y) \<longrightarrow> x = y; \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option fst (m x) = map_option fst (m y) \<longrightarrow> x = y; c y = Some z; c x = Some z; ((z, x) \<in> ran m) = (c x = Some z)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>\<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option snd (m x) = map_option snd (m y) \<longrightarrow> x = y; \<forall>x\<in>dom m. \<forall>y\<in>dom m. map_option fst (m x) = map_option fst (m y) \<longrightarrow> x = y; c y = Some z; c x = Some z; ((z, x) \<in> ran m) = (c x = Some z); ((z, y) \<in> ran m) = (c y = Some z)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>x y z a aa. ?y71 x y z a aa (typ_at' (?T70 x y z a aa) (?p70 x y z a aa) (?s70 x y z a aa)) \<equiv>\<^sup>? \<lambda>x y z a aa. ?y71 x y z a aa (typ_at' (?T70 x y z a aa) (?p70 x y z a aa) (?s70 x y z a aa\<lparr>ksMachineState := ksMachineState (?s70 x y z a aa)\<lparr>irq_state := ?f70 x y z a aa (irq_state (ksMachineState (?s70 x y z a aa)))\<rparr>\<rparr>))