theory ADT_IF

lemma silc_inv_cur:
  "silc_inv (current_aag s) st s = silc_inv initial_aag st s" apply (rule iffI) apply (subst initial_aag_bak[where s=s]) apply (rule silc_inv_pasSubject_update) apply simp+ apply (simp add: current_aag_def) apply (subst the_subject_of_aag_domain[where l = "pasSubject initial_aag"]) apply (rule cur_domain_subject_s0) apply (blast intro: cur_domain_subject_s0) apply (simp add: current_aag_def) apply (rule silc_inv_pasSubject_update) apply blast+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silc_inv (current_aag s) st s = silc_inv initial_aag st s proof (prove)
goal (2 subgoals):
 1. silc_inv (current_aag s) st s \<Longrightarrow> silc_inv initial_aag st s
 2. silc_inv initial_aag st s \<Longrightarrow> silc_inv (current_aag s) st s proof (prove)
goal (2 subgoals):
 1. silc_inv (current_aag s) st s \<Longrightarrow> silc_inv (current_aag s\<lparr>pasSubject := the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal))\<rparr>) st s
 2. silc_inv initial_aag st s \<Longrightarrow> silc_inv (current_aag s) st s proof (prove)
goal (4 subgoals):
 1. silc_inv (current_aag s) st s \<Longrightarrow> silc_inv (current_aag s) st s
 2. silc_inv (current_aag s) st s \<Longrightarrow> pas_wellformed_noninterference (current_aag s)
 3. silc_inv (current_aag s) st s \<Longrightarrow> the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal)) \<in> pasDomainAbs (current_aag s) ?d5
 4. silc_inv initial_aag st s \<Longrightarrow> silc_inv (current_aag s) st s proof (prove)
goal (2 subgoals):
 1. silc_inv (current_aag s) st s \<Longrightarrow> the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal)) \<in> pasDomainAbs (current_aag s) ?d5
 2. silc_inv initial_aag st s \<Longrightarrow> silc_inv (current_aag s) st s proof (prove)
goal (2 subgoals):
 1. silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s))\<rparr>) st s \<Longrightarrow> the_elem (pasDomainAbs initial_aag (cur_domain s0_internal)) \<in> pasDomainAbs initial_aag ?d5
 2. silc_inv initial_aag st s \<Longrightarrow> silc_inv (current_aag s) st s proof (prove)
goal (3 subgoals):
 1. silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s))\<rparr>) st s \<Longrightarrow> pas_cur_domain initial_aag s0_internal
 2. silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s))\<rparr>) st s \<Longrightarrow> pasSubject initial_aag \<in> pasDomainAbs initial_aag ?d5
 3. silc_inv initial_aag st s \<Longrightarrow> silc_inv (current_aag s) st s proof (prove)
goal (2 subgoals):
 1. silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s))\<rparr>) st s \<Longrightarrow> pasSubject initial_aag \<in> pasDomainAbs initial_aag ?d5
 2. silc_inv initial_aag st s \<Longrightarrow> silc_inv (current_aag s) st s proof (prove)
goal (1 subgoal):
 1. silc_inv initial_aag st s \<Longrightarrow> silc_inv (current_aag s) st s proof (prove)
goal (1 subgoal):
 1. silc_inv initial_aag st s \<Longrightarrow> silc_inv (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s))\<rparr>) st s proof (prove)
goal (3 subgoals):
 1. silc_inv initial_aag st s \<Longrightarrow> silc_inv initial_aag st s
 2. silc_inv initial_aag st s \<Longrightarrow> pas_wellformed_noninterference initial_aag
 3. silc_inv initial_aag st s \<Longrightarrow> the_elem (pasDomainAbs initial_aag (cur_domain s)) \<in> pasDomainAbs initial_aag ?d19 proof (prove)
goal:
No subgoals!