theory Scratch

imports Main

begin

lemma foo:
  "\<And>a aa b ba ab bb bc.
       pasDomainAbs initial_aag (cur_domain b)
       \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) \<Longrightarrow>
       u = Partition a \<Longrightarrow>
       s = ((aa, b), ba) \<Longrightarrow>
       s' = ((ab, bb), bc) \<Longrightarrow>
       states_equiv_for
        (\<lambda>x. pasObjectAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
        (\<lambda>x. pasIRQAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
        (\<lambda>x. pasASIDAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
        (\<lambda>x. pasDomainAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a))
        (\<lambda>x. ptr_range x 12) b bb \<Longrightarrow>
       pasDomainAbs initial_aag (cur_domain b)
       \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) \<longrightarrow>
       cur_domain b = cur_domain bb \<and>
       globals_equiv b bb \<and>
       scheduler_action b = scheduler_action bb \<and>
       work_units_completed b = work_units_completed bb \<and>
       equiv_irq_state (machine_state b) (machine_state bb) \<and>
       (user_modes ba \<longrightarrow> aa = ab) \<and>
       ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb \<Longrightarrow>
       pasDomainAbs initial_aag (cur_domain bb)
       \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel a) \<longrightarrow>
       cur_domain b = cur_domain bb \<and>
       globals_equiv b bb \<and>
       scheduler_action b = scheduler_action bb \<and>
       work_units_completed b = work_units_completed bb \<and>
       equiv_irq_state (machine_state b) (machine_state bb) \<and>
       (user_modes ba \<longrightarrow> aa = ab) \<and>
       ba = bc \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap b bb \<Longrightarrow>
       (user_modes ba \<longrightarrow> aa = ab) \<and> ba = bc
  "
  using [[simp_legacy_precond = true ]]
  apply simp
  apply fast
  apply (drule(1) mp, simp)
  apply clarify



end