[STATEMENT]
lemma ft_foldl_impl: "al_foldl ft_\<alpha> ft_invar ft_foldl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_foldl ft_\<alpha> (\<lambda>_. True) ft_foldl
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s f \<sigma>. True \<Longrightarrow> ft_foldl f \<sigma> s = foldl f \<sigma> (ft_\<alpha> s)
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.foldl_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_foldr_impl: "al_foldr ft_\<alpha> ft_invar ft_foldr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_foldr ft_\<alpha> (\<lambda>_. True) ft_foldr
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s f \<sigma>. True \<Longrightarrow> ft_foldr f s \<sigma> = foldr f (ft_\<alpha> s) \<sigma>
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.foldr_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_foldl_cunfold[code_unfold]:
  "List.foldl f \<sigma> (ft_\<alpha> t) = ft_foldl f \<sigma> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldl f \<sigma> (ft_\<alpha> t) = ft_foldl f \<sigma> t
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.foldl_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_foldr_cunfold[code_unfold]:
  "List.foldr f (ft_\<alpha> t) \<sigma> = ft_foldr f t \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr f (ft_\<alpha> t) \<sigma> = ft_foldr f t \<sigma>
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.foldr_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_app_impl: "al_app ft_\<alpha> ft_invar ft_app"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_app ft_\<alpha> (\<lambda>_. True) ft_app
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> ft_\<alpha> (ft_app s s') = ft_\<alpha> s @ ft_\<alpha> s'
 2. \<And>s s'. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.app_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_annot_impl: "al_annot ft_\<alpha> ft_invar ft_annot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_annot ft_\<alpha> (\<lambda>_. True) ft_annot
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ft_annot s = sum_list (map snd (ft_\<alpha> s))
[PROOF STEP]
apply (auto simp add: ft_defs FingerTree.annot_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ft_splits_impl: "al_splits ft_\<alpha> ft_invar ft_splits"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. al_splits ft_\<alpha> (\<lambda>_. True) ft_splits
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s p i l e a r. \<lbrakk>True; \<forall>a b. p a \<longrightarrow> p (a + b); \<not> p i; p (i + sum_list (map snd (ft_\<alpha> s))); ft_splits p i s = (l, (e, a), r)\<rbrakk> \<Longrightarrow> ft_\<alpha> s = ft_\<alpha> l @ (e, a) # ft_\<alpha> r \<and> \<not> p (i + sum_list (map snd (ft_\<alpha> l))) \<and> p (i + sum_list (map snd (ft_\<alpha> l)) + a) \<and> True \<and> True
[PROOF STEP]
apply (unfold ft_defs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s p i l e a r. \<lbrakk>True; \<forall>a b. p a \<longrightarrow> p (a + b); \<not> p i; p (i + sum_list (map snd (FingerTree.toList s))); FingerTree.splitTree p i s = (l, (e, a), r)\<rbrakk> \<Longrightarrow> FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r \<and> \<not> p (i + sum_list (map snd (FingerTree.toList l))) \<and> p (i + sum_list (map snd (FingerTree.toList l)) + a) \<and> True \<and> True
[PROOF STEP]
apply (simp only: FingerTree.annot_correct[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s p i l e a r. \<lbrakk>True; \<forall>a b. p a \<longrightarrow> p (a + b); \<not> p i; p (i + FingerTree.annot s); FingerTree.splitTree p i s = (l, (e, a), r)\<rbrakk> \<Longrightarrow> FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r \<and> \<not> p (i + FingerTree.annot l) \<and> p (i + FingerTree.annot l + a) \<and> True \<and> True
[PROOF STEP]
apply (frule (3) FingerTree.splitTree_correct(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s p i l e a r. \<lbrakk>True; \<forall>a b. p a \<longrightarrow> p (a + b); \<not> p i; p (i + FingerTree.annot s); FingerTree.splitTree p i s = (l, (e, a), r); FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r\<rbrakk> \<Longrightarrow> FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r \<and> \<not> p (i + FingerTree.annot l) \<and> p (i + FingerTree.annot l + a) \<and> True \<and> True
[PROOF STEP]
apply (frule (3) FingerTree.splitTree_correct(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s p i l e a r. \<lbrakk>True; \<forall>a b. p a \<longrightarrow> p (a + b); \<not> p i; p (i + FingerTree.annot s); FingerTree.splitTree p i s = (l, (e, a), r); FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r; \<not> p (i + FingerTree.annot l)\<rbrakk> \<Longrightarrow> FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r \<and> \<not> p (i + FingerTree.annot l) \<and> p (i + FingerTree.annot l + a) \<and> True \<and> True
[PROOF STEP]
apply (frule (3) FingerTree.splitTree_correct(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s p i l e a r. \<lbrakk>True; \<forall>a b. p a \<longrightarrow> p (a + b); \<not> p i; p (i + FingerTree.annot s); FingerTree.splitTree p i s = (l, (e, a), r); FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r; \<not> p (i + FingerTree.annot l); p (i + FingerTree.annot l + a)\<rbrakk> \<Longrightarrow> FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r \<and> \<not> p (i + FingerTree.annot l) \<and> p (i + FingerTree.annot l + a) \<and> True \<and> True
[PROOF STEP]
apply (simp only: FingerTree.annot_correct[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s p i l e a r. \<lbrakk>True; \<forall>a b. p a \<longrightarrow> p (a + b); \<not> p i; p (i + FingerTree.annot s); FingerTree.splitTree p i s = (l, (e, a), r); FingerTree.toList s = FingerTree.toList l @ (e, a) # FingerTree.toList r; \<not> p (i + FingerTree.annot l); p (i + FingerTree.annot l + a)\<rbrakk> \<Longrightarrow> FingerTree.toList l @ (e, a) # FingerTree.toList r = FingerTree.toList l @ (e, a) # FingerTree.toList r \<and> \<not> False \<and> True \<and> True \<and> True
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rel_mset_Plus_gen:
  assumes "rel_mset A m m'"
  assumes "rel_mset A n n'"
  shows "rel_mset A (m+n) (m'+n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_mset A (m + n) (m' + n')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rel_mset A m m'
rel_mset A n n'

goal (1 subgoal):
 1. rel_mset A (m + n) (m' + n')
[PROOF STEP]
by induction (auto simp: algebra_simps dest: rel_mset_Plus)


[STATEMENT]
lemma rel_mset_single:
  assumes "A x y"
  shows "rel_mset A {#x#} {#y#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_mset A {#x#} {#y#}
[PROOF STEP]
unfolding rel_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs ys. mset xs = {#x#} \<and> mset ys = {#y#} \<and> list_all2 A xs ys
[PROOF STEP]
apply (rule exI[where x="[x]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys. mset [x] = {#x#} \<and> mset ys = {#y#} \<and> list_all2 A [x] ys
[PROOF STEP]
apply (rule exI[where x="[y]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset [x] = {#x#} \<and> mset [y] = {#y#} \<and> list_all2 A [x] [y]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A x y

goal (1 subgoal):
 1. mset [x] = {#x#} \<and> mset [y] = {#y#} \<and> list_all2 A [x] [y]
[PROOF STEP]
by auto


[STATEMENT]
lemma rel_mset_Minus:
  assumes BIU: "bi_unique A"
  shows "\<lbrakk> rel_mset A m n; A x y \<rbrakk> \<Longrightarrow> rel_mset A (m-{#x#}) (n-{#y#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_mset A m n; A x y\<rbrakk> \<Longrightarrow> rel_mset A (m - {#x#}) (n - {#y#})
[PROOF STEP]
unfolding rel_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>xs ys. mset xs = m \<and> mset ys = n \<and> list_all2 A xs ys; A x y\<rbrakk> \<Longrightarrow> \<exists>xs ys. mset xs = m - {#x#} \<and> mset ys = n - {#y#} \<and> list_all2 A xs ys
[PROOF STEP]
proof clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>A x y; m = mset xs; list_all2 A xs ys; n = mset ys\<rbrakk> \<Longrightarrow> \<exists>xsa. mset xsa = mset xs - {#x#} \<and> (\<exists>ysa. mset ysa = mset ys - {#y#} \<and> list_all2 A xsa ysa)
[PROOF STEP]
fix ml nl
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>A x y; m = mset xs; list_all2 A xs ys; n = mset ys\<rbrakk> \<Longrightarrow> \<exists>xsa. mset xsa = mset xs - {#x#} \<and> (\<exists>ysa. mset ysa = mset ys - {#y#} \<and> list_all2 A xsa ysa)
[PROOF STEP]
assume A: "A x y"
[PROOF STATE]
proof (state)
this:
A x y

goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>A x y; m = mset xs; list_all2 A xs ys; n = mset ys\<rbrakk> \<Longrightarrow> \<exists>xsa. mset xsa = mset xs - {#x#} \<and> (\<exists>ysa. mset ysa = mset ys - {#y#} \<and> list_all2 A xsa ysa)
[PROOF STEP]
assume R: "list_all2 A ml nl"
[PROOF STATE]
proof (state)
this:
list_all2 A ml nl

goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>A x y; m = mset xs; list_all2 A xs ys; n = mset ys\<rbrakk> \<Longrightarrow> \<exists>xsa. mset xsa = mset xs - {#x#} \<and> (\<exists>ysa. mset ysa = mset ys - {#y#} \<and> list_all2 A xsa ysa)
[PROOF STEP]
show "\<exists>ml'. mset ml' = mset ml - {#x#} \<and>
                 (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
proof (cases "x\<in>set ml")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
 2. x \<notin> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> set ml

goal (2 subgoals):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
 2. x \<notin> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
have "y \<notin> set nl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> set nl
[PROOF STEP]
using A R
[PROOF STATE]
proof (prove)
using this:
A x y
list_all2 A ml nl

goal (1 subgoal):
 1. y \<notin> set nl
[PROOF STEP]
apply (auto simp: in_set_conv_decomp list_all2_append2 list_all2_Cons2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ys zs us z zsa. \<lbrakk>A x y; nl = ys @ y # zs; ml = us @ z # zsa; length us = length ys; length zsa = length zs; list_all2 A us ys; A z y; list_all2 A zsa zs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using False BIU[unfolded bi_unique_alt_def]
[PROOF STATE]
proof (prove)
using this:
x \<notin> set ml
left_unique A \<and> right_unique A

goal (1 subgoal):
 1. \<And>ys zs us z zsa. \<lbrakk>A x y; nl = ys @ y # zs; ml = us @ z # zsa; length us = length ys; length zsa = length zs; list_all2 A us ys; A z y; list_all2 A zsa zs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto dest: left_uniqueD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
y \<notin> set nl

goal (2 subgoals):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
 2. x \<notin> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
with False R
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set ml
list_all2 A ml nl
y \<notin> set nl
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> set ml
list_all2 A ml nl
y \<notin> set nl

goal (1 subgoal):
 1. \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
by (auto simp: diff_single_trivial in_multiset_in_set)
[PROOF STATE]
proof (state)
this:
\<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')

goal (1 subgoal):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> set ml

goal (1 subgoal):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set ml
[PROOF STEP]
obtain ml1 ml2 where [simp]: "ml=ml1@x#ml2"
[PROOF STATE]
proof (prove)
using this:
x \<in> set ml

goal (1 subgoal):
 1. (\<And>ml1 ml2. ml = ml1 @ x # ml2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: in_set_conv_decomp)
[PROOF STATE]
proof (state)
this:
ml = ml1 @ x # ml2

goal (1 subgoal):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ml = ml1 @ x # ml2
[PROOF STEP]
obtain nl1 nl2 where [simp]: "nl=nl1@y#nl2"
      and LA: "list_all2 A ml1 nl1" "list_all2 A ml2 nl2"
[PROOF STATE]
proof (prove)
using this:
ml = ml1 @ x # ml2

goal (1 subgoal):
 1. (\<And>nl1 nl2. \<lbrakk>nl = nl1 @ y # nl2; list_all2 A ml1 nl1; list_all2 A ml2 nl2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A R
[PROOF STATE]
proof (prove)
using this:
ml = ml1 @ x # ml2
A x y
list_all2 A ml nl

goal (1 subgoal):
 1. (\<And>nl1 nl2. \<lbrakk>nl = nl1 @ y # nl2; list_all2 A ml1 nl1; list_all2 A ml2 nl2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp: in_set_conv_decomp list_all2_append1 list_all2_Cons1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>us z zs. \<lbrakk>\<And>nl1 nl2. \<lbrakk>us @ z # zs = nl1 @ y # nl2; list_all2 A ml1 nl1; list_all2 A ml2 nl2\<rbrakk> \<Longrightarrow> thesis; A x y; nl = us @ z # zs; length us = length ml1; length zs = length ml2; list_all2 A ml1 us; A x z; list_all2 A ml2 zs\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using BIU[unfolded bi_unique_alt_def]
[PROOF STATE]
proof (prove)
using this:
left_unique A \<and> right_unique A

goal (1 subgoal):
 1. \<And>us z zs. \<lbrakk>\<And>nl1 nl2. \<lbrakk>us @ z # zs = nl1 @ y # nl2; list_all2 A ml1 nl1; list_all2 A ml2 nl2\<rbrakk> \<Longrightarrow> thesis; A x y; nl = us @ z # zs; length us = length ml1; length zs = length ml2; list_all2 A ml1 us; A x z; list_all2 A ml2 zs\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto dest: right_uniqueD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nl = nl1 @ y # nl2
list_all2 A ml1 nl1
list_all2 A ml2 nl2

goal (1 subgoal):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
have
      "mset (ml1@ml2) = mset ml - {#x#}"
      "mset (nl1@nl2) = mset nl - {#y#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (ml1 @ ml2) = mset ml - {#x#} &&& mset (nl1 @ nl2) = mset nl - {#y#}
[PROOF STEP]
using R
[PROOF STATE]
proof (prove)
using this:
list_all2 A ml nl

goal (1 subgoal):
 1. mset (ml1 @ ml2) = mset ml - {#x#} &&& mset (nl1 @ nl2) = mset nl - {#y#}
[PROOF STEP]
by (auto simp: algebra_simps add_implies_diff union_assoc)
[PROOF STATE]
proof (state)
this:
mset (ml1 @ ml2) = mset ml - {#x#}
mset (nl1 @ nl2) = mset nl - {#y#}

goal (1 subgoal):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mset (ml1 @ ml2) = mset ml - {#x#}
mset (nl1 @ nl2) = mset nl - {#y#}

goal (1 subgoal):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
have "list_all2 A (ml1@ml2) (nl1@nl2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 A (ml1 @ ml2) (nl1 @ nl2)
[PROOF STEP]
by (rule list_all2_appendI) fact+
[PROOF STATE]
proof (state)
this:
list_all2 A (ml1 @ ml2) (nl1 @ nl2)

goal (1 subgoal):
 1. x \<in> set ml \<Longrightarrow> \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mset (ml1 @ ml2) = mset ml - {#x#}
mset (nl1 @ nl2) = mset nl - {#y#}
list_all2 A (ml1 @ ml2) (nl1 @ nl2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset (ml1 @ ml2) = mset ml - {#x#}
mset (nl1 @ nl2) = mset nl - {#y#}
list_all2 A (ml1 @ ml2) (nl1 @ nl2)

goal (1 subgoal):
 1. \<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ml'. mset ml' = mset ml - {#x#} \<and> (\<exists>nl'. mset nl' = mset nl - {#y#} \<and> list_all2 A ml' nl')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_mset_Minus_gen:
  assumes BIU: "bi_unique A"
  assumes "rel_mset A m m'"
  assumes "rel_mset A n n'"
  shows "rel_mset A (m-n) (m'-n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_mset A (m - n) (m' - n')
[PROOF STEP]
using assms(3,2)
[PROOF STATE]
proof (prove)
using this:
rel_mset A n n'
rel_mset A m m'

goal (1 subgoal):
 1. rel_mset A (m - n) (m' - n')
[PROOF STEP]
apply (induction R\<equiv>A _ _ rule: rel_mset_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. rel_mset A m m' \<Longrightarrow> rel_mset A (m - {#}) (m' - {#})
 2. \<And>a b M N. \<lbrakk>A a b; rel_mset A M N; rel_mset A m m' \<Longrightarrow> rel_mset A (m - M) (m' - N); rel_mset A m m'\<rbrakk> \<Longrightarrow> rel_mset A (m - add_mset a M) (m' - add_mset b N)
[PROOF STEP]
apply (auto dest: rel_mset_Minus[OF BIU] simp: algebra_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pcr_count:
  assumes "bi_unique A"
  shows "rel_fun (rel_mset A) (rel_fun A (=)) count count"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel_mset A) (rel_fun A (=)) count count
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>rel_mset A x y; A xa ya\<rbrakk> \<Longrightarrow> count x xa = count y ya
[PROOF STEP]
unfolding rel_mset_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>\<exists>xs ys. mset xs = x \<and> mset ys = y \<and> list_all2 A xs ys; A xa ya\<rbrakk> \<Longrightarrow> count x xa = count y ya
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa ya xs ys. \<lbrakk>A xa ya; list_all2 A xs ys\<rbrakk> \<Longrightarrow> count (mset xs) xa = count (mset ys) ya
[PROOF STEP]
subgoal for x y xs ys
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A x y; list_all2 A xs ys\<rbrakk> \<Longrightarrow> count (mset xs) x = count (mset ys) y
[PROOF STEP]
apply (rotate_tac,induction xs ys rule: list_all2_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A x y \<Longrightarrow> count (mset []) x = count (mset []) y
 2. \<And>xa x' ls ls'. \<lbrakk>A xa x'; list_all2 A ls ls'; A x y \<Longrightarrow> count (mset ls) x = count (mset ls') y; A x y\<rbrakk> \<Longrightarrow> count (mset (xa # ls)) x = count (mset (x' # ls')) y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bi_unique A

goal (2 subgoals):
 1. A x y \<Longrightarrow> count (mset []) x = count (mset []) y
 2. \<And>xa x' ls ls'. \<lbrakk>A xa x'; list_all2 A ls ls'; A x y \<Longrightarrow> count (mset ls) x = count (mset ls') y; A x y\<rbrakk> \<Longrightarrow> count (mset (xa # ls)) x = count (mset (x' # ls')) y
[PROOF STEP]
by (auto simp: bi_unique_alt_def left_uniqueD right_uniqueD)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rel2p_mset[rel2p]: "rel2p (\<langle>A\<rangle>mset_rel) = rel_mset (rel2p A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel2p (\<langle>A\<rangle>mset_rel) = rel_mset (rel2p A)
[PROOF STEP]
by (simp add: mset_rel_def)


[STATEMENT]
lemma p2re_mset[p2rel]: "p2rel (rel_mset A) = \<langle>p2rel A\<rangle>mset_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p2rel (rel_mset A) = \<langle>p2rel A\<rangle>mset_rel
[PROOF STEP]
by (simp add: mset_rel_def)


[STATEMENT]
lemma mset_rel_empty[simp]:
  "(a,{#})\<in>\<langle>A\<rangle>mset_rel \<longleftrightarrow> a={#}"
  "({#},b)\<in>\<langle>A\<rangle>mset_rel \<longleftrightarrow> b={#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a, {#}) \<in> \<langle>A\<rangle>mset_rel) = (a = {#}) &&& (({#}, b) \<in> \<langle>A\<rangle>mset_rel) = (b = {#})
[PROOF STEP]
by (auto simp: mset_rel_def p2rel_def rel_mset_def)


[STATEMENT]
lemma param_mset_empty[param]: "({#},{#}) \<in> \<langle>A\<rangle>mset_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({#}, {#}) \<in> \<langle>A\<rangle>mset_rel
[PROOF STEP]
by simp


[STATEMENT]
lemma param_mset_Plus[param]: "((+),(+))\<in>\<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((+), (+)) \<in> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel
[PROOF STEP]
apply (rule rel2pD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel2p (\<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel) (+) (+)
[PROOF STEP]
apply (simp add: rel2p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel_mset (rel2p A)) (rel_fun (rel_mset (rel2p A)) (rel_mset (rel2p A))) (+) (+)
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>rel_mset (rel2p A) x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> rel_mset (rel2p A) (x + xa) (y + ya)
[PROOF STEP]
by (rule rel_mset_Plus_gen)


[STATEMENT]
lemma param_mset_add[param]: "(add_mset, add_mset) \<in> A \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (add_mset, add_mset) \<in> A \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel
[PROOF STEP]
apply (rule rel2pD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel2p (A \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel) add_mset add_mset
[PROOF STEP]
apply (simp add: rel2p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel2p A) (rel_fun (rel_mset (rel2p A)) (rel_mset (rel2p A))) add_mset add_mset
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>rel2p A x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> rel_mset (rel2p A) (add_mset x xa) (add_mset y ya)
[PROOF STEP]
by (rule rel_mset_Plus)


[STATEMENT]
lemma param_mset_minus[param]: "\<lbrakk>single_valued A; single_valued (A\<inverse>)\<rbrakk>
  \<Longrightarrow> ((-), (-)) \<in> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued A; single_valued (A\<inverse>)\<rbrakk> \<Longrightarrow> ((-), (-)) \<in> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel
[PROOF STEP]
apply (rule rel2pD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued A; single_valued (A\<inverse>)\<rbrakk> \<Longrightarrow> rel2p (\<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>mset_rel) (-) (-)
[PROOF STEP]
apply (simp add: rel2p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued A; single_valued (A\<inverse>)\<rbrakk> \<Longrightarrow> rel_fun (rel_mset (rel2p A)) (rel_fun (rel_mset (rel2p A)) (rel_mset (rel2p A))) (-) (-)
[PROOF STEP]
apply (intro rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>single_valued A; single_valued (A\<inverse>); rel_mset (rel2p A) x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> rel_mset (rel2p A) (x - xa) (y - ya)
[PROOF STEP]
apply (rule rel_mset_Minus_gen)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y xa ya. \<lbrakk>single_valued A; single_valued (A\<inverse>); rel_mset (rel2p A) x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> bi_unique (rel2p A)
 2. \<And>x y xa ya. \<lbrakk>single_valued A; single_valued (A\<inverse>); rel_mset (rel2p A) x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> rel_mset (rel2p A) x y
 3. \<And>x y xa ya. \<lbrakk>single_valued A; single_valued (A\<inverse>); rel_mset (rel2p A) x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> rel_mset (rel2p A) xa ya
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued A; single_valued (A\<inverse>); rel_mset (rel2p A) x_ y_; rel_mset (rel2p A) xa_ ya_\<rbrakk> \<Longrightarrow> bi_unique (rel2p A)
[PROOF STEP]
apply (unfold IS_LEFT_UNIQUE_def[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued A; IS_LEFT_UNIQUE A; rel_mset (rel2p A) x_ y_; rel_mset (rel2p A) xa_ ya_\<rbrakk> \<Longrightarrow> bi_unique (rel2p A)
[PROOF STEP]
by (simp add: prop2p bi_unique_alt_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y xa ya. \<lbrakk>single_valued A; single_valued (A\<inverse>); rel_mset (rel2p A) x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> rel_mset (rel2p A) x y
 2. \<And>x y xa ya. \<lbrakk>single_valued A; single_valued (A\<inverse>); rel_mset (rel2p A) x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> rel_mset (rel2p A) xa ya
[PROOF STEP]
apply (simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>single_valued A; single_valued (A\<inverse>); rel_mset (rel2p A) x y; rel_mset (rel2p A) xa ya\<rbrakk> \<Longrightarrow> rel_mset (rel2p A) xa ya
[PROOF STEP]
apply (simp; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma param_count[param]: "\<lbrakk>single_valued A; single_valued (A\<inverse>)\<rbrakk> \<Longrightarrow> (count,count)\<in>\<langle>A\<rangle>mset_rel \<rightarrow> A \<rightarrow> nat_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued A; single_valued (A\<inverse>)\<rbrakk> \<Longrightarrow> (count, count) \<in> \<langle>A\<rangle>mset_rel \<rightarrow> A \<rightarrow> nat_rel
[PROOF STEP]
apply (rule rel2pD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued A; single_valued (A\<inverse>)\<rbrakk> \<Longrightarrow> rel2p (\<langle>A\<rangle>mset_rel \<rightarrow> A \<rightarrow> nat_rel) count count
[PROOF STEP]
apply (simp add: prop2p rel2p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>right_unique (rel2p A); left_unique (rel2p A)\<rbrakk> \<Longrightarrow> rel_fun (rel_mset (rel2p A)) (rel_fun (rel2p A) (=)) count count
[PROOF STEP]
apply (rule pcr_count)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>right_unique (rel2p A); left_unique (rel2p A)\<rbrakk> \<Longrightarrow> bi_unique (rel2p A)
[PROOF STEP]
apply (simp add: bi_unique_alt_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma param_set_mset[param]:
  shows "(set_mset, set_mset) \<in> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set_mset, set_mset) \<in> \<langle>A\<rangle>mset_rel \<rightarrow> \<langle>A\<rangle>set_rel
[PROOF STEP]
apply (rule rel2pD; simp add: rel2p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel_mset (rel2p A)) (rel_set (rel2p A)) set_mset set_mset
[PROOF STEP]
by (rule multiset.set_transfer)


[STATEMENT]
lemma mset_is_empty_param[param]: "(mset_is_empty,mset_is_empty) \<in> \<langle>A\<rangle>mset_rel \<rightarrow> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mset_is_empty, mset_is_empty) \<in> \<langle>A\<rangle>mset_rel \<rightarrow> bool_rel
[PROOF STEP]
unfolding mset_rel_def mset_is_empty_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>m. m = {#}, \<lambda>m. m = {#}) \<in> p2rel (rel_mset (rel2p A)) \<rightarrow> bool_rel
[PROOF STEP]
by (auto simp: p2rel_def rel_mset_def intro: nres_relI)


[STATEMENT]
lemma [def_pat_rules]:
  "{#} \<equiv> op_mset_empty"
  "add_mset \<equiv> op_mset_insert"
  "(=) $b${#} \<equiv> op_mset_is_empty$b"
  "(=) ${#}$b \<equiv> op_mset_is_empty$b"
  "(+) $a$b \<equiv> op_mset_plus$a$b"
  "(-) $a$b \<equiv> op_mset_minus$a$b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (({#} \<equiv> op_mset_empty) &&& (add_mset \<equiv> op_mset_insert) &&& (=) $ b $ {#} \<equiv> op_mset_is_empty $ b) &&& ((=) $ {#} $ b \<equiv> op_mset_is_empty $ b) &&& ((+) $ a $ b \<equiv> op_mset_plus $ a $ b) &&& (-) $ a $ b \<equiv> op_mset_minus $ a $ b
[PROOF STEP]
by (auto intro!: eq_reflection simp: algebra_simps)


[STATEMENT]
lemma [def_pat_rules]:
  "(+) $b$(add_mset$x${#}) \<equiv> op_mset_insert$x$b"
  "(+) $(add_mset$x${#})$b \<equiv> op_mset_insert$x$b"
  "(-) $b$(add_mset$x${#}) \<equiv> op_mset_delete$x$b"
  "(<) $0$(count$a$x) \<equiv> op_mset_contains$x$a"
  "(\<in>) $x$(set_mset$a) \<equiv> op_mset_contains$x$a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((+) $ b $ (add_mset $ x $ {#}) \<equiv> op_mset_insert $ x $ b) &&& (+) $ (add_mset $ x $ {#}) $ b \<equiv> op_mset_insert $ x $ b) &&& ((-) $ b $ (add_mset $ x $ {#}) \<equiv> op_mset_delete $ x $ b) &&& ((<) $ 0 $ (count $ a $ x) \<equiv> op_mset_contains $ x $ a) &&& (\<in>) $ x $ (set_mset $ a) \<equiv> op_mset_contains $ x $ a
[PROOF STEP]
by (auto intro!: eq_reflection simp: algebra_simps)


[STATEMENT]
lemma fold_custom_empty:
    "{#} = op_custom_empty"
    "op_mset_empty = op_custom_empty"
    "mop_mset_empty = RETURN op_custom_empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#} = op_custom_empty &&& op_mset_empty = op_custom_empty &&& mop_mset_empty = RETURN op_custom_empty
[PROOF STEP]
unfolding op_custom_empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {#} = op_mset_empty &&& op_mset_empty = op_mset_empty &&& mop_mset_empty = RETURN op_mset_empty
[PROOF STEP]
by simp_all


[STATEMENT]
lemma if_type'':
  "\<lbrakk>type_bexpr \<Gamma> e t; pred_entailment P t;
    has_type  \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P';
    has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P'';
    pred_entailment P' {e}; pred_entailment P'' {bexp_neg e};
    P''' = restrict_preds_to_vars (((Imp e) ` (P' - {e})) \<union> ((Imp (bexp_neg e)) ` (P'' - {bexp_neg e}))) {v. stable \<S>' v}\<rbrakk>
\<Longrightarrow> has_type \<Gamma> \<S> P (Stmt.If e c\<^sub>1 c\<^sub>2) \<Gamma>' \<S>' P'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type_bexpr \<Gamma> e t; pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> has_type \<Gamma> \<S> P (Stmt.If e c\<^sub>1 c\<^sub>2) \<Gamma>' \<S>' P'''
[PROOF STEP]
apply(erule (3) if_type,simp+)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp.Not e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp.Not e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp.Not e) ` (P'' - {bexp.Not e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> pred_entailment P' (restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp.Not e) ` (P'' - {bexp.Not e})) {v. local.stable \<S>' v})
 2. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> pred_entailment P'' P'''
 3. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P' \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S>' P'''
 4. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P'' \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S>' P'''
[PROOF STEP]
apply(auto simp: pred_entailment_def pred_def image_def restrict_preds_to_vars_def)[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> pred_entailment P'' P'''
 2. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P' \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S>' P'''
 3. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P'' \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S>' P'''
[PROOF STEP]
apply(auto simp: pred_entailment_def pred_def image_def restrict_preds_to_vars_def)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P' \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S>' P'''
 2. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P'' \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S>' P'''
[PROOF STEP]
apply(clarsimp simp: tyenv_wellformed_def mds_consistent_def stable_def image_def restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>mds p x. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' (mds AsmNoWrite, mds AsmNoReadOrWrite) P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp.Not e)) c\<^sub>2 \<Gamma>' (mds AsmNoWrite, mds AsmNoReadOrWrite) P''; pred_entailment P' {e}; pred_entailment P'' {bexp.Not e}; P''' = {ea. ((\<exists>x\<in>P' - {e}. ea = Imp e x) \<or> (\<exists>x\<in>P'' - {bexp.Not e}. ea = Imp (bexp.Not e) x)) \<and> bexp_vars ea \<subseteq> {v. v \<in> mds AsmNoWrite \<or> v \<in> mds AsmNoReadOrWrite}}; \<S>' = (mds AsmNoWrite, mds AsmNoReadOrWrite); dom \<Gamma>' = {x. x \<notin> \<C> \<and> (x \<in> mds AsmNoWrite \<or> x \<in> mds AsmNoReadOrWrite)}; \<forall>p\<in>P'. \<forall>x\<in>bexp_vars p. x \<in> mds AsmNoWrite \<or> x \<in> mds AsmNoReadOrWrite; types_wellformed \<Gamma>'; types_stable \<Gamma>' (mds AsmNoWrite, mds AsmNoReadOrWrite); x \<in> bexp_vars p; (\<exists>x\<in>P' - {e}. p = Imp e x) \<or> (\<exists>x\<in>P'' - {bexp.Not e}. p = Imp (bexp.Not e) x); bexp_vars p \<subseteq> {v. v \<in> mds AsmNoWrite \<or> v \<in> mds AsmNoReadOrWrite}; x \<notin> mds AsmNoReadOrWrite\<rbrakk> \<Longrightarrow> x \<in> mds AsmNoWrite
 2. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P'' \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S>' P'''
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' \<S>' P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp_neg e)) c\<^sub>2 \<Gamma>' \<S>' P''; pred_entailment P' {e}; pred_entailment P'' {bexp_neg e}; P''' = restrict_preds_to_vars (Imp e ` (P' - {e}) \<union> Imp (bexp_neg e) ` (P'' - {bexp_neg e})) {v. local.stable \<S>' v}\<rbrakk> \<Longrightarrow> \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P'' \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S>' P'''
[PROOF STEP]
apply(clarsimp simp: tyenv_wellformed_def mds_consistent_def stable_def image_def restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mds p x. \<lbrakk>pred_entailment P t; has_type \<Gamma> \<S> (add_pred P \<S> e) c\<^sub>1 \<Gamma>' (mds AsmNoWrite, mds AsmNoReadOrWrite) P'; has_type \<Gamma> \<S> (add_pred P \<S> (bexp.Not e)) c\<^sub>2 \<Gamma>' (mds AsmNoWrite, mds AsmNoReadOrWrite) P''; pred_entailment P' {e}; pred_entailment P'' {bexp.Not e}; P''' = {ea. ((\<exists>x\<in>P' - {e}. ea = Imp e x) \<or> (\<exists>x\<in>P'' - {bexp.Not e}. ea = Imp (bexp.Not e) x)) \<and> bexp_vars ea \<subseteq> {v. v \<in> mds AsmNoWrite \<or> v \<in> mds AsmNoReadOrWrite}}; \<S>' = (mds AsmNoWrite, mds AsmNoReadOrWrite); dom \<Gamma>' = {x. x \<notin> \<C> \<and> (x \<in> mds AsmNoWrite \<or> x \<in> mds AsmNoReadOrWrite)}; \<forall>p\<in>P''. \<forall>x\<in>bexp_vars p. x \<in> mds AsmNoWrite \<or> x \<in> mds AsmNoReadOrWrite; types_wellformed \<Gamma>'; types_stable \<Gamma>' (mds AsmNoWrite, mds AsmNoReadOrWrite); x \<in> bexp_vars p; (\<exists>x\<in>P' - {e}. p = Imp e x) \<or> (\<exists>x\<in>P'' - {bexp.Not e}. p = Imp (bexp.Not e) x); bexp_vars p \<subseteq> {v. v \<in> mds AsmNoWrite \<or> v \<in> mds AsmNoReadOrWrite}; x \<notin> mds AsmNoReadOrWrite\<rbrakk> \<Longrightarrow> x \<in> mds AsmNoWrite
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma \<C>_simp[simp]:
  "\<C> = {control_X, control_Y, control_Z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<C> = {control_X, control_Y, control_Z}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<C> = {control_X, control_Y, control_Z}
[PROOF STEP]
have "\<C> = control_var_of ` {x. x = X \<or> x = Y \<or> x = Z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<C> = control_var_of ` {x. x = X \<or> x = Y \<or> x = Z}
[PROOF STEP]
by (simp add: \<C>_def \<C>_vars_def UNION_singleton_eq_range)
[PROOF STATE]
proof (state)
this:
\<C> = control_var_of ` {x. x = X \<or> x = Y \<or> x = Z}

goal (1 subgoal):
 1. \<C> = {control_X, control_Y, control_Z}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<C> = control_var_of ` {x. x = X \<or> x = Y \<or> x = Z}

goal (1 subgoal):
 1. \<C> = {control_X, control_Y, control_Z}
[PROOF STEP]
have "{x. x = X \<or> x = Y \<or> x = Z} = {X, Y, Z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. x = X \<or> x = Y \<or> x = Z} = {X, Y, Z}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. x = X \<or> x = Y \<or> x = Z} = {X, Y, Z}

goal (1 subgoal):
 1. \<C> = {control_X, control_Y, control_Z}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<C> = control_var_of ` {X, Y, Z}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<C> = control_var_of ` {X, Y, Z}

goal (1 subgoal):
 1. \<C> = {control_X, control_Y, control_Z}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<C> = {control_X, control_Y, control_Z}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma type_aexpr_Load:
  "v \<notin> dom \<Gamma> \<Longrightarrow> type_aexpr \<Gamma> (Load v) (dma_type v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<notin> dom \<Gamma> \<Longrightarrow> type_aexpr \<Gamma> (Load v) (dma_type v)
[PROOF STEP]
apply(insert type_aexpr[of \<Gamma> "Load v", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<notin> dom \<Gamma>; type_aexpr \<Gamma> (Load v) (to_total \<Gamma> v)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Load v) (dma_type v)
[PROOF STEP]
apply(simp add: to_total_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma type_aexpr_Load':
  "v \<in> dom \<Gamma> \<Longrightarrow> t = (the (\<Gamma> v)) \<Longrightarrow> type_aexpr \<Gamma> (Load v) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> dom \<Gamma>; t = the (\<Gamma> v)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Load v) t
[PROOF STEP]
apply(insert type_aexpr[of \<Gamma> "Load v", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> dom \<Gamma>; t = the (\<Gamma> v); type_aexpr \<Gamma> (Load v) (to_total \<Gamma> v)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Load v) t
[PROOF STEP]
apply(simp add: to_total_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma type_aexpr_Add:
  "x \<notin> dom \<Gamma> \<Longrightarrow> y \<notin> dom \<Gamma> \<Longrightarrow>
   type_aexpr \<Gamma> (Add x y) (\<Union> {dma_type x, dma_type y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> dom \<Gamma>; y \<notin> dom \<Gamma>\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Add x y) (\<Union> {dma_type x, dma_type y})
[PROOF STEP]
apply(insert type_aexpr[of \<Gamma> "Add x y", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> dom \<Gamma>; y \<notin> dom \<Gamma>; type_aexpr \<Gamma> (Add x y) (to_total \<Gamma> x \<union> to_total \<Gamma> y)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Add x y) (\<Union> {dma_type x, dma_type y})
[PROOF STEP]
apply(simp add: to_total_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma type_aexpr_Add':
  "x \<notin> dom \<Gamma> \<Longrightarrow> y \<in> dom \<Gamma> \<Longrightarrow> t = (the (\<Gamma> y)) \<Longrightarrow>
   type_aexpr \<Gamma> (Add x y) (\<Union> {dma_type x, t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> dom \<Gamma>; y \<in> dom \<Gamma>; t = the (\<Gamma> y)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Add x y) (\<Union> {dma_type x, t})
[PROOF STEP]
apply(insert type_aexpr[of \<Gamma> "Add x y", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> dom \<Gamma>; y \<in> dom \<Gamma>; t = the (\<Gamma> y); type_aexpr \<Gamma> (Add x y) (to_total \<Gamma> x \<union> to_total \<Gamma> y)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Add x y) (\<Union> {dma_type x, t})
[PROOF STEP]
apply(simp add: to_total_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma type_aexpr_Add'':
  "x \<in> dom \<Gamma> \<Longrightarrow> y \<notin> dom \<Gamma> \<Longrightarrow> t = (the (\<Gamma> x)) \<Longrightarrow>
   type_aexpr \<Gamma> (Add x y) (\<Union> {t, dma_type y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> dom \<Gamma>; y \<notin> dom \<Gamma>; t = the (\<Gamma> x)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Add x y) (\<Union> {t, dma_type y})
[PROOF STEP]
apply(insert type_aexpr[of \<Gamma> "Add x y", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> dom \<Gamma>; y \<notin> dom \<Gamma>; t = the (\<Gamma> x); type_aexpr \<Gamma> (Add x y) (to_total \<Gamma> x \<union> to_total \<Gamma> y)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Add x y) (\<Union> {t, dma_type y})
[PROOF STEP]
apply(simp add: to_total_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma type_aexpr_Add''':
  "x \<in> dom \<Gamma> \<Longrightarrow> y \<in> dom \<Gamma> \<Longrightarrow> t = (the (\<Gamma> x)) \<Longrightarrow> t' = (the (\<Gamma> y)) \<Longrightarrow>
   type_aexpr \<Gamma> (Add x y) (\<Union> {t, t'})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> dom \<Gamma>; y \<in> dom \<Gamma>; t = the (\<Gamma> x); t' = the (\<Gamma> y)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Add x y) (\<Union> {t, t'})
[PROOF STEP]
apply(insert type_aexpr[of \<Gamma> "Add x y", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> dom \<Gamma>; y \<in> dom \<Gamma>; t = the (\<Gamma> x); t' = the (\<Gamma> y); type_aexpr \<Gamma> (Add x y) (to_total \<Gamma> x \<union> to_total \<Gamma> y)\<rbrakk> \<Longrightarrow> type_aexpr \<Gamma> (Add x y) (\<Union> {t, t'})
[PROOF STEP]
apply(simp add: to_total_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma type_aexpr_Const[simp]:
  "type_aexpr \<Gamma> (Const c) {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. type_aexpr \<Gamma> (Const c) {}
[PROOF STEP]
apply(insert type_aexpr[of \<Gamma> "Const c", simplified],simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma control_vars_cases:
  "control_X \<in> \<C>_vars v \<Longrightarrow> v = X"
  "control_Y \<in> \<C>_vars v \<Longrightarrow> v = Y"
  "control_Z \<in> \<C>_vars v \<Longrightarrow> v = Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (control_X \<in> \<C>_vars v \<Longrightarrow> v = X) &&& (control_Y \<in> \<C>_vars v \<Longrightarrow> v = Y) &&& (control_Z \<in> \<C>_vars v \<Longrightarrow> v = Z)
[PROOF STEP]
by(case_tac v, auto)+


[STATEMENT]
lemma mem_is_different[simp, intro]:
  "mem x = A \<Longrightarrow> mem y \<noteq> A \<Longrightarrow> \<not> ev\<^sub>B  mem (Same y (Load x))"
  "mem x = A \<Longrightarrow> mem y \<noteq> A \<Longrightarrow> \<not> ev\<^sub>B  mem (Same x (Load y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>mem x = A; mem y \<noteq> A\<rbrakk> \<Longrightarrow> \<not> ev\<^sub>B mem (Same y (Load x))) &&& (\<lbrakk>mem x = A; mem y \<noteq> A\<rbrakk> \<Longrightarrow> \<not> ev\<^sub>B mem (Same x (Load y)))
[PROOF STEP]
by fastforce+


[STATEMENT]
lemma restrict_preds_to_vars_empty[simp]:
  "restrict_preds_to_vars {} V = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict_preds_to_vars {} V = {}
[PROOF STEP]
apply(simp add: restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma restrict_preds_to_vars_idemp[simp]:
  "restrict_preds_to_vars (restrict_preds_to_vars P V) V =
   restrict_preds_to_vars P 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
[PROOF STEP]
apply(simp add: restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma restrict_preds_to_vars_insert1[simp]:
  "(\<forall>x\<in>bexp_vars a. x \<in> V) \<Longrightarrow> restrict_preds_to_vars (insert a P) V = (insert a (restrict_preds_to_vars P V))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>bexp_vars a. x \<in> V \<Longrightarrow> restrict_preds_to_vars (insert a P) V = insert a (restrict_preds_to_vars P V)
[PROOF STEP]
apply(simp add: restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>bexp_vars a. x \<in> V \<Longrightarrow> {e. (e = a \<or> e \<in> P) \<and> bexp_vars e \<subseteq> V} = insert a {e \<in> P. bexp_vars e \<subseteq> V}
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma restrict_preds_to_vars_insert2[simp]:
  "(\<exists>x\<in>bexp_vars a. x \<notin> V) \<Longrightarrow> restrict_preds_to_vars (insert a P) V = ((restrict_preds_to_vars P V))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>bexp_vars a. x \<notin> V \<Longrightarrow> restrict_preds_to_vars (insert a P) V = restrict_preds_to_vars P V
[PROOF STEP]
apply(simp add: restrict_preds_to_vars_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>bexp_vars a. x \<notin> V \<Longrightarrow> {e. (e = a \<or> e \<in> P) \<and> bexp_vars e \<subseteq> V} = {e \<in> P. bexp_vars e \<subseteq> V}
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "pred_entailment P {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_entailment P {}
[PROOF STEP]
by(simp add: pred_entailment_def pred_def)


[STATEMENT]
lemma [simp]: "e \<in> P \<Longrightarrow> pred_entailment P {e}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<in> P \<Longrightarrow> pred_entailment P {e}
[PROOF STEP]
by(blast intro: subset_entailment)


[STATEMENT]
lemma [simp]: "FF \<in> P \<Longrightarrow> pred_entailment P Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FF \<in> P \<Longrightarrow> pred_entailment P Q
[PROOF STEP]
by(auto simp: pred_entailment_def pred_def)