[STATEMENT]
lemma swap_vars_sifum_secure:
  "com_sifum_secure (swap_vars,(\<lambda>_. {}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. com_sifum_secure (swap_vars, \<lambda>_. {})
[PROOF STEP]
apply(insert swap_vars_typed[OF HOL.refl HOL.refl HOL.refl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<Gamma>' \<S>' P'. has_type Map.empty ({}, {}) {} swap_vars \<Gamma>' \<S>' P' \<Longrightarrow> com_sifum_secure (swap_vars, \<lambda>_. {})
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma>' a b x. has_type Map.empty ({}, {}) {} swap_vars \<Gamma>' (a, b) x \<Longrightarrow> com_sifum_secure (swap_vars, \<lambda>_. {})
[PROOF STEP]
apply(rule typed_secure)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma>' a b x. has_type Map.empty ({}, {}) {} swap_vars \<Gamma>' (a, b) x \<Longrightarrow> has_type (\<Gamma>_of_mds (\<lambda>_. {})) (\<S>_of_mds (\<lambda>_. {})) {} swap_vars (?\<Gamma>'8 \<Gamma>' a b x) (?\<S>'8 \<Gamma>' a b x) (?P'8 \<Gamma>' a b x)
 2. \<And>\<Gamma>' a b x. has_type Map.empty ({}, {}) {} swap_vars \<Gamma>' (a, b) x \<Longrightarrow> mds_yields_stable_types (\<lambda>_. {})
[PROOF STEP]
apply(fastforce simp: \<Gamma>_of_mds_def \<S>_of_mds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma>' a b x. has_type Map.empty ({}, {}) {} swap_vars \<Gamma>' (a, b) x \<Longrightarrow> mds_yields_stable_types (\<lambda>_. {})
[PROOF STEP]
apply(auto simp: mds_yields_stable_types_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pred_entailment_singleton_by_case_distinction:
  "Imp e f \<in> P \<Longrightarrow> Imp (bexp.Not e) f \<in> P \<Longrightarrow> pred_entailment P {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Imp e f \<in> P; Imp (bexp.Not e) f \<in> P\<rbrakk> \<Longrightarrow> pred_entailment P {f}
[PROOF STEP]
apply(clarsimp simp: pred_entailment_def pred_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mem. \<lbrakk>Imp e f \<in> P; Imp (bexp.Not e) f \<in> P; \<forall>x\<in>P. ev\<^sub>B mem x\<rbrakk> \<Longrightarrow> ev\<^sub>B mem f
[PROOF STEP]
apply(case_tac "ev\<^sub>B mem e")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>mem. \<lbrakk>Imp e f \<in> P; Imp (bexp.Not e) f \<in> P; \<forall>x\<in>P. ev\<^sub>B mem x; ev\<^sub>B mem e\<rbrakk> \<Longrightarrow> ev\<^sub>B mem f
 2. \<And>mem. \<lbrakk>Imp e f \<in> P; Imp (bexp.Not e) f \<in> P; \<forall>x\<in>P. ev\<^sub>B mem x; \<not> ev\<^sub>B mem e\<rbrakk> \<Longrightarrow> ev\<^sub>B mem f
[PROOF STEP]
apply fastforce+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma restrict_preds_to_vars_nest [simp]:
  "restrict_preds_to_vars (restrict_preds_to_vars P V) V' = restrict_preds_to_vars P (V \<inter> V')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_preds_to_vars (restrict_preds_to_vars P V) V' = restrict_preds_to_vars P (V \<inter> V')
[PROOF STEP]
apply(auto simp: restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma restrict_preds_to_vars_imp_image1 [simp]:
  "\<not> bexp_vars e \<subseteq> V \<Longrightarrow> restrict_preds_to_vars (Imp e ` P) V = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bexp_vars e \<subseteq> V \<Longrightarrow> restrict_preds_to_vars (Imp e ` P) V = {}
[PROOF STEP]
apply(auto simp: restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma restrict_preds_to_vars_imp_image2 [simp]:
  "bexp_vars e \<subseteq> V \<Longrightarrow> restrict_preds_to_vars (Imp e ` P) V = ((Imp e) ` (restrict_preds_to_vars P V))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bexp_vars e \<subseteq> V \<Longrightarrow> restrict_preds_to_vars (Imp e ` P) V = Imp e ` restrict_preds_to_vars P V
[PROOF STEP]
apply(auto simp: restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma insert_minus1 [simp]:
  "x = y \<Longrightarrow> (insert x A) - {y} = (A - {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y \<Longrightarrow> insert x A - {y} = A - {y}
[PROOF STEP]
by auto


[STATEMENT]
lemma insert_minus2 [simp]:
  "x \<noteq> y \<Longrightarrow> (insert x A) - {y} = insert x (A - {y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> insert x A - {y} = insert x (A - {y})
[PROOF STEP]
by auto