theory ADT_IF_Refine

lemma ADT_A_if_Init_Fin_serial:
  "uop_sane uop \<Longrightarrow> Init_Fin_serial (ADT_A_if uop) s0 (full_invs_if \<inter> {s. step_restrict s})" apply (simp add: Init_Fin_serial_def) apply (rule conjI) apply (rule global_automata_refine.abs_serial[OF haskell_to_abs]) apply (simp add: uop_sane_def uop_nonempty_def) apply (fastforce simp: step_restrict_def has_srel_state_def) apply (clarsimp simp add: doUserOp_H_if_def) apply (frule use_valid[OF _ doUserOp_if_no_interrupt]) apply simp+ apply (unfold_locales) apply (clarsimp simp: ADT_A_if_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_sane uop \<Longrightarrow> Init_Fin_serial (ADT_A_if uop) s0 (full_invs_if \<inter> {s. step_restrict s}) proof (prove)
goal (1 subgoal):
 1. uop_sane uop \<Longrightarrow> serial_system (ADT_A_if uop) (full_invs_if \<inter> Collect step_restrict) \<and> Init_Fin_serial_axioms (ADT_A_if uop) s0 (full_invs_if \<inter> Collect step_restrict) proof (prove)
goal (2 subgoals):
 1. uop_sane uop \<Longrightarrow> serial_system (ADT_A_if uop) (full_invs_if \<inter> Collect step_restrict)
 2. uop_sane uop \<Longrightarrow> Init_Fin_serial_axioms (ADT_A_if uop) s0 (full_invs_if \<inter> Collect step_restrict) proof (prove)
goal (5 subgoals):
 1. uop_sane uop \<Longrightarrow> uop_nonempty uop
 2. \<And>s. \<lbrakk>uop_sane uop; s \<in> full_invs_if \<inter> {s. step_restrict s}\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> full_invs_if' \<and> (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation)
 3. \<And>s e t. \<lbrakk>uop_sane uop; (s, e, t) \<in> doUserOp_H_if uop\<rbrakk> \<Longrightarrow> e \<noteq> Some Interrupt
 4. uop_sane uop \<Longrightarrow> True
 5. uop_sane uop \<Longrightarrow> Init_Fin_serial_axioms (ADT_A_if uop) s0 (full_invs_if \<inter> Collect step_restrict) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>uop_sane uop; s \<in> full_invs_if \<inter> {s. step_restrict s}\<rbrakk> \<Longrightarrow> \<exists>s'. s' \<in> full_invs_if' \<and> (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation)
 2. \<And>s e t. \<lbrakk>uop_sane uop; (s, e, t) \<in> doUserOp_H_if uop\<rbrakk> \<Longrightarrow> e \<noteq> Some Interrupt
 3. uop_sane uop \<Longrightarrow> True
 4. uop_sane uop \<Longrightarrow> Init_Fin_serial_axioms (ADT_A_if uop) s0 (full_invs_if \<inter> Collect step_restrict) proof (prove)
goal (3 subgoals):
 1. \<And>s e t. \<lbrakk>uop_sane uop; (s, e, t) \<in> doUserOp_H_if uop\<rbrakk> \<Longrightarrow> e \<noteq> Some Interrupt
 2. uop_sane uop \<Longrightarrow> True
 3. uop_sane uop \<Longrightarrow> Init_Fin_serial_axioms (ADT_A_if uop) s0 (full_invs_if \<inter> Collect step_restrict) proof (prove)
goal (3 subgoals):
 1. \<And>ab bb tc s'. \<lbrakk>uop_sane uop; ((Some Interrupt, tc), s') \<in> fst (doUserOp_if uop ab bb)\<rbrakk> \<Longrightarrow> False
 2. uop_sane uop \<Longrightarrow> True
 3. uop_sane uop \<Longrightarrow> Init_Fin_serial_axioms (ADT_A_if uop) s0 (full_invs_if \<inter> Collect step_restrict) proof (prove)
goal (4 subgoals):
 1. \<And>ab bb tc s'. \<lbrakk>uop_sane uop; ((Some Interrupt, tc), s') \<in> fst (doUserOp_if uop ab bb)\<rbrakk> \<Longrightarrow> K (uop_sane uop) bb
 2. \<And>ab bb tc s'. \<lbrakk>uop_sane uop; ((Some Interrupt, tc), s') \<in> fst (doUserOp_if uop ab bb); fst (Some Interrupt, tc) \<noteq> Some Interrupt\<rbrakk> \<Longrightarrow> False
 3. uop_sane uop \<Longrightarrow> True
 4. uop_sane uop \<Longrightarrow> Init_Fin_serial_axioms (ADT_A_if uop) s0 (full_invs_if \<inter> Collect step_restrict) proof (prove)
goal (1 subgoal):
 1. uop_sane uop \<Longrightarrow> Init_Fin_serial_axioms (ADT_A_if uop) s0 (full_invs_if \<inter> Collect step_restrict) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>uop_sane uop; s' \<in> full_invs_if \<inter> Collect step_restrict\<rbrakk> \<Longrightarrow> s' \<in> Init (ADT_A_if uop) (Fin (ADT_A_if uop) s')
 2. uop_sane uop \<Longrightarrow> Init (ADT_A_if uop) s0 \<subseteq> full_invs_if \<inter> Collect step_restrict proof (prove)
goal:
No subgoals!