[STATEMENT]
lemma find_first_some:
  assumes "x \<in> set xs"
  obtains i where "find_first x xs = Some i" "i < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>find_first x xs = Some i; i < length xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> set xs

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>find_first x xs = Some i; i < length xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis order_refl take_all find_first_some_strong)


[STATEMENT]
lemma find_first_append:
  "find_first x (ys @ zs) =
    (case find_first x ys of None \<Rightarrow> map_option (\<lambda>i. i + length ys) (find_first x zs) | Some a \<Rightarrow> Some a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x (ys @ zs) = (case find_first x ys of None \<Rightarrow> map_option (\<lambda>i. i + length ys) (find_first x zs) | Some a \<Rightarrow> Some a)
[PROOF STEP]
by (induct ys) (auto simp: option.map_comp comp_def map_option.identity split: option.splits)


[STATEMENT]
lemma find_first_first:
  assumes "i < length xs" "x \<notin> set (take i xs)" "xs ! i = x"
  shows "find_first x xs = Some i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
let ?ys = "take i xs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
let ?zs = "drop i xs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
have "?zs ! 0 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop i xs ! 0 = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length xs
x \<notin> set (take i xs)
xs ! i = x

goal (1 subgoal):
 1. drop i xs ! 0 = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop i xs ! 0 = x

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
hence "find_first x ?zs = Some 0"
[PROOF STATE]
proof (prove)
using this:
drop i xs ! 0 = x

goal (1 subgoal):
 1. find_first x (drop i xs) = Some 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
drop i xs ! 0 = x
i < length xs
x \<notin> set (take i xs)
xs ! i = x

goal (1 subgoal):
 1. find_first x (drop i xs) = Some 0
[PROOF STEP]
by (cases ?zs) auto
[PROOF STATE]
proof (state)
this:
find_first x (drop i xs) = Some 0

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
find_first x (drop i xs) = Some 0

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
have "find_first x ?ys = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x (take i xs) = None
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < length xs
x \<notin> set (take i xs)
xs ! i = x

goal (1 subgoal):
 1. find_first x (take i xs) = None
[PROOF STEP]
by (simp add: find_first_none)
[PROOF STATE]
proof (state)
this:
find_first x (take i xs) = None

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
find_first x (drop i xs) = Some 0
find_first x (take i xs) = None
[PROOF STEP]
have "find_first x (?ys @ ?zs) = Some i"
[PROOF STATE]
proof (prove)
using this:
find_first x (drop i xs) = Some 0
find_first x (take i xs) = None

goal (1 subgoal):
 1. find_first x (take i xs @ drop i xs) = Some i
[PROOF STEP]
unfolding find_first_append
[PROOF STATE]
proof (prove)
using this:
find_first x (drop i xs) = Some 0
find_first x (take i xs) = None

goal (1 subgoal):
 1. (case find_first x (take i xs) of None \<Rightarrow> map_option (\<lambda>ia. ia + length (take i xs)) (find_first x (drop i xs)) | Some x \<Rightarrow> Some x) = Some i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_first x (drop i xs) = Some 0
find_first x (take i xs) = None
i < length xs
x \<notin> set (take i xs)
xs ! i = x

goal (1 subgoal):
 1. (case find_first x (take i xs) of None \<Rightarrow> map_option (\<lambda>ia. ia + length (take i xs)) (find_first x (drop i xs)) | Some x \<Rightarrow> Some x) = Some i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_first x (take i xs @ drop i xs) = Some i

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
find_first x (take i xs @ drop i xs) = Some i

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_first x (take i xs @ drop i xs) = Some i
i < length xs
x \<notin> set (take i xs)
xs ! i = x

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_first x xs = Some i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_first_prefix:
  assumes "find_first x xs = Some i" "i < n"
  shows "find_first x (take n xs) = Some i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x (take n xs) = Some i
[PROOF STEP]
proof (rule find_first_first)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. i < length (take n xs)
 2. x \<notin> set (take i (take n xs))
 3. take n xs ! i = x
[PROOF STEP]
show "i < length (take n xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (take n xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some i
i < n

goal (1 subgoal):
 1. i < length (take n xs)
[PROOF STEP]
by (simp add: find_first_correct)
[PROOF STATE]
proof (state)
this:
i < length (take n xs)

goal (2 subgoals):
 1. x \<notin> set (take i (take n xs))
 2. take n xs ! i = x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<notin> set (take i (take n xs))
 2. take n xs ! i = x
[PROOF STEP]
have "x \<notin> set (take i xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> set (take i xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some i
i < n

goal (1 subgoal):
 1. x \<notin> set (take i xs)
[PROOF STEP]
by (simp add: find_first_correct)
[PROOF STATE]
proof (state)
this:
x \<notin> set (take i xs)

goal (2 subgoals):
 1. x \<notin> set (take i (take n xs))
 2. take n xs ! i = x
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
find_first x xs = Some i
i < n
x \<notin> set (take i xs)
[PROOF STEP]
show "x \<notin> set (take i (take n xs))"
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some i
i < n
x \<notin> set (take i xs)

goal (1 subgoal):
 1. x \<notin> set (take i (take n xs))
[PROOF STEP]
by (simp add: min.absorb1)
[PROOF STATE]
proof (state)
this:
x \<notin> set (take i (take n xs))

goal (1 subgoal):
 1. take n xs ! i = x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. take n xs ! i = x
[PROOF STEP]
show "take n xs ! i = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take n xs ! i = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some i
i < n

goal (1 subgoal):
 1. take n xs ! i = x
[PROOF STEP]
by (simp add: find_first_correct)
[PROOF STATE]
proof (state)
this:
take n xs ! i = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_first_later:
  assumes "i < length xs" "j < length xs" "i < j"
  assumes "xs ! i = x" "xs ! j = x"
  shows "find_first x xs \<noteq> Some j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x xs \<noteq> Some j
[PROOF STEP]
proof (cases "x \<in> set (take i xs)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
 2. x \<notin> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> set (take i xs)

goal (2 subgoals):
 1. x \<in> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
 2. x \<notin> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (take i xs)
[PROOF STEP]
obtain k where "find_first x xs = Some k" "k < i"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (take i xs)

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>find_first x xs = Some k; k < i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> set (take i xs)
i < length xs
j < length xs
i < j
xs ! i = x
xs ! j = x

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>find_first x xs = Some k; k < i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: find_first_some_strong)
[PROOF STATE]
proof (state)
this:
find_first x xs = Some k
k < i

goal (2 subgoals):
 1. x \<in> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
 2. x \<notin> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some k
k < i

goal (1 subgoal):
 1. find_first x xs \<noteq> Some j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some k
k < i
i < length xs
j < length xs
i < j
xs ! i = x
xs ! j = x

goal (1 subgoal):
 1. find_first x xs \<noteq> Some j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_first x xs \<noteq> Some j

goal (1 subgoal):
 1. x \<notin> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> set (take i xs)

goal (1 subgoal):
 1. x \<notin> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
[PROOF STEP]
hence "find_first x xs = Some i"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set (take i xs)

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<notin> set (take i xs)
i < length xs
j < length xs
i < j
xs ! i = x
xs ! j = x

goal (1 subgoal):
 1. find_first x xs = Some i
[PROOF STEP]
by (simp add: find_first_first)
[PROOF STATE]
proof (state)
this:
find_first x xs = Some i

goal (1 subgoal):
 1. x \<notin> set (take i xs) \<Longrightarrow> find_first x xs \<noteq> Some j
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some i

goal (1 subgoal):
 1. find_first x xs \<noteq> Some j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_first x xs = Some i
i < length xs
j < length xs
i < j
xs ! i = x
xs ! j = x

goal (1 subgoal):
 1. find_first x xs \<noteq> Some j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
find_first x xs \<noteq> Some j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_first_in_map:
  assumes "length xs \<le> length ys" "find_first n xs = Some i"
  shows "fmlookup (fmap_of_list (zip xs ys)) n = Some (ys ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmlookup (fmap_of_list (zip xs ys)) n = Some (ys ! i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs \<le> length ys
find_first n xs = Some i

goal (1 subgoal):
 1. fmlookup (fmap_of_list (zip xs ys)) n = Some (ys ! i)
[PROOF STEP]
proof (induction xs arbitrary: ys i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys i. \<lbrakk>length [] \<le> length ys; find_first n [] = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip [] ys)) n = Some (ys ! i)
 2. \<And>a xs ys i. \<lbrakk>\<And>ys i. \<lbrakk>length xs \<le> length ys; find_first n xs = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip xs ys)) n = Some (ys ! i); length (a # xs) \<le> length ys; find_first n (a # xs) = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip (a # xs) ys)) n = Some (ys ! i)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length xs \<le> length ?ys; find_first n xs = Some ?i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip xs ?ys)) n = Some (?ys ! ?i)
length (x # xs) \<le> length ys
find_first n (x # xs) = Some i

goal (2 subgoals):
 1. \<And>ys i. \<lbrakk>length [] \<le> length ys; find_first n [] = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip [] ys)) n = Some (ys ! i)
 2. \<And>a xs ys i. \<lbrakk>\<And>ys i. \<lbrakk>length xs \<le> length ys; find_first n xs = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip xs ys)) n = Some (ys ! i); length (a # xs) \<le> length ys; find_first n (a # xs) = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip (a # xs) ys)) n = Some (ys ! i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length xs \<le> length ?ys; find_first n xs = Some ?i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip xs ?ys)) n = Some (?ys ! ?i)
length (x # xs) \<le> length ys
find_first n (x # xs) = Some i
[PROOF STEP]
obtain y ys' where "ys = y # ys'"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs \<le> length ?ys; find_first n xs = Some ?i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip xs ?ys)) n = Some (?ys ! ?i)
length (x # xs) \<le> length ys
find_first n (x # xs) = Some i

goal (1 subgoal):
 1. (\<And>y ys'. ys = y # ys' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Skolem_list_nth le_0_eq length_greater_0_conv less_nat_zero_code list.set_cases listrel_Cons1 listrel_iff_nth nth_mem)
[PROOF STATE]
proof (state)
this:
ys = y # ys'

goal (2 subgoals):
 1. \<And>ys i. \<lbrakk>length [] \<le> length ys; find_first n [] = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip [] ys)) n = Some (ys ! i)
 2. \<And>a xs ys i. \<lbrakk>\<And>ys i. \<lbrakk>length xs \<le> length ys; find_first n xs = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip xs ys)) n = Some (ys ! i); length (a # xs) \<le> length ys; find_first n (a # xs) = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip (a # xs) ys)) n = Some (ys ! i)
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length xs \<le> length ?ys; find_first n xs = Some ?i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip xs ?ys)) n = Some (?ys ! ?i)
length (x # xs) \<le> length ys
find_first n (x # xs) = Some i
ys = y # ys'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length xs \<le> length ?ys; find_first n xs = Some ?i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip xs ?ys)) n = Some (?ys ! ?i)
length (x # xs) \<le> length ys
find_first n (x # xs) = Some i
ys = y # ys'

goal (1 subgoal):
 1. fmlookup (fmap_of_list (zip (x # xs) ys)) n = Some (ys ! i)
[PROOF STEP]
by (cases "x = n") auto
[PROOF STATE]
proof (state)
this:
fmlookup (fmap_of_list (zip (x # xs) ys)) n = Some (ys ! i)

goal (1 subgoal):
 1. \<And>ys i. \<lbrakk>length [] \<le> length ys; find_first n [] = Some i\<rbrakk> \<Longrightarrow> fmlookup (fmap_of_list (zip [] ys)) n = Some (ys ! i)
[PROOF STEP]
qed auto


[STATEMENT]
lemma common_prefix_find:
  assumes "z \<in> set (common_prefix xs ys)"
  shows "find_first z xs = find_first z ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first z xs = find_first z ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<in> set (common_prefix xs ys)

goal (1 subgoal):
 1. find_first z xs = find_first z ys
[PROOF STEP]
by (induct xs ys rule: common_prefix.induct) auto


[STATEMENT]
lemma find_first_insert_nth_eq:
  assumes "n \<le> length xs" "x \<notin> set (take n xs)"
  shows "find_first x (insert_nth n x xs) = Some n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x (insert_nth n x xs) = Some n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<le> length xs
x \<notin> set (take n xs)

goal (1 subgoal):
 1. find_first x (insert_nth n x xs) = Some n
[PROOF STEP]
by (auto simp: find_first_append find_first_none split: option.splits)


[STATEMENT]
lemma insert_nth_induct:
  fixes P :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
    and a0 :: "nat"
    and a1 :: "'a"
    and a2 :: "'a list"
  assumes "\<And>x xs. P 0 x xs"
    and "\<And>n x y ys. P n x ys \<Longrightarrow> P (Suc n) x (y # ys)"
    and "\<And>n x. P (Suc n) x []"
  shows "P a0 a1 a2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P a0 a1 a2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P 0 ?x ?xs
P ?n ?x ?ys \<Longrightarrow> P (Suc ?n) ?x (?y # ?ys)
P (Suc ?n) ?x []

goal (1 subgoal):
 1. P a0 a1 a2
[PROOF STEP]
apply induction_schema
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>P a0 a1 a2. \<lbrakk>\<And>x__ xs__. \<lbrakk>a0 = 0; a1 = x__; a2 = xs__\<rbrakk> \<Longrightarrow> P; \<And>n__ x__ ys__ y__. \<lbrakk>a0 = Suc n__; a1 = x__; a2 = y__ # ys__\<rbrakk> \<Longrightarrow> P; \<And>n__ x__. \<lbrakk>a0 = Suc n__; a1 = x__; a2 = []\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
 2. wf ?R2
 3. \<And>n__ x__ ys__ y__. ((n__, x__, ys__), Suc n__, x__, y__ # ys__) \<in> ?R2
[PROOF STEP]
apply pat_completeness
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf ?R2
 2. \<And>n__ x__ ys__ y__. ((n__, x__, ys__), Suc n__, x__, y__ # ys__) \<in> ?R2
[PROOF STEP]
apply lexicographic_order
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma find_first_insert_nth_neq:
  assumes "x \<noteq> y"
  shows "find_first x (insert_nth n y xs) = map_option (\<lambda>i. if i < n then i else Suc i) (find_first x xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x (insert_nth n y xs) = map_option (\<lambda>i. if i < n then i else Suc i) (find_first x xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. find_first x (insert_nth n y xs) = map_option (\<lambda>i. if i < n then i else Suc i) (find_first x xs)
[PROOF STEP]
proof (induction n y xs rule: insert_nth_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xa xs. x \<noteq> xa \<Longrightarrow> find_first x (insert_nth 0 xa xs) = map_option (\<lambda>i. if i < 0 then i else Suc i) (find_first x xs)
 2. \<And>n xa y ys. \<lbrakk>x \<noteq> xa \<Longrightarrow> find_first x (insert_nth n xa ys) = map_option (\<lambda>i. if i < n then i else Suc i) (find_first x ys); x \<noteq> xa\<rbrakk> \<Longrightarrow> find_first x (insert_nth (Suc n) xa (y # ys)) = map_option (\<lambda>i. if i < Suc n then i else Suc i) (find_first x (y # ys))
 3. \<And>n xa. x \<noteq> xa \<Longrightarrow> find_first x (insert_nth (Suc n) xa []) = map_option (\<lambda>i. if i < Suc n then i else Suc i) (find_first x [])
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
x \<noteq> x_ \<Longrightarrow> find_first x (insert_nth n_ x_ ys_) = map_option (\<lambda>i. if i < n_ then i else Suc i) (find_first x ys_)
x \<noteq> x_

goal (3 subgoals):
 1. \<And>xa xs. x \<noteq> xa \<Longrightarrow> find_first x (insert_nth 0 xa xs) = map_option (\<lambda>i. if i < 0 then i else Suc i) (find_first x xs)
 2. \<And>n xa y ys. \<lbrakk>x \<noteq> xa \<Longrightarrow> find_first x (insert_nth n xa ys) = map_option (\<lambda>i. if i < n then i else Suc i) (find_first x ys); x \<noteq> xa\<rbrakk> \<Longrightarrow> find_first x (insert_nth (Suc n) xa (y # ys)) = map_option (\<lambda>i. if i < Suc n then i else Suc i) (find_first x (y # ys))
 3. \<And>n xa. x \<noteq> xa \<Longrightarrow> find_first x (insert_nth (Suc n) xa []) = map_option (\<lambda>i. if i < Suc n then i else Suc i) (find_first x [])
[PROOF STEP]
note insert_nth_take_drop[simp del]
[PROOF STATE]
proof (state)
this:
insert_nth ?n ?x ?xs = take ?n ?xs @ [?x] @ drop ?n ?xs

goal (3 subgoals):
 1. \<And>xa xs. x \<noteq> xa \<Longrightarrow> find_first x (insert_nth 0 xa xs) = map_option (\<lambda>i. if i < 0 then i else Suc i) (find_first x xs)
 2. \<And>n xa y ys. \<lbrakk>x \<noteq> xa \<Longrightarrow> find_first x (insert_nth n xa ys) = map_option (\<lambda>i. if i < n then i else Suc i) (find_first x ys); x \<noteq> xa\<rbrakk> \<Longrightarrow> find_first x (insert_nth (Suc n) xa (y # ys)) = map_option (\<lambda>i. if i < Suc n then i else Suc i) (find_first x (y # ys))
 3. \<And>n xa. x \<noteq> xa \<Longrightarrow> find_first x (insert_nth (Suc n) xa []) = map_option (\<lambda>i. if i < Suc n then i else Suc i) (find_first x [])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_first x (insert_nth (Suc n_) x_ (y_ # ys_)) = map_option (\<lambda>i. if i < Suc n_ then i else Suc i) (find_first x (y_ # ys_))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y_ \<Longrightarrow> map_option Suc (find_first x (insert_nth n_ x_ ys_)) = map_option (\<lambda>i. if i < Suc n_ then i else Suc i) (map_option Suc (find_first x ys_))
[PROOF STEP]
apply (subst 2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<noteq> y_ \<Longrightarrow> x \<noteq> x_
 2. x \<noteq> y_ \<Longrightarrow> map_option Suc (map_option (\<lambda>i. if i < n_ then i else Suc i) (find_first x ys_)) = map_option (\<lambda>i. if i < Suc n_ then i else Suc i) (map_option Suc (find_first x ys_))
[PROOF STEP]
apply (rule 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y_ \<Longrightarrow> map_option Suc (map_option (\<lambda>i. if i < n_ then i else Suc i) (find_first x ys_)) = map_option (\<lambda>i. if i < Suc n_ then i else Suc i) (map_option Suc (find_first x ys_))
[PROOF STEP]
unfolding option.map_comp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y_ \<Longrightarrow> map_option (Suc \<circ> (\<lambda>i. if i < n_ then i else Suc i)) (find_first x ys_) = map_option ((\<lambda>i. if i < Suc n_ then i else Suc i) \<circ> Suc) (find_first x ys_)
[PROOF STEP]
apply (rule option.map_cong0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<noteq> y_; z \<in> set_option (find_first x ys_)\<rbrakk> \<Longrightarrow> (Suc \<circ> (\<lambda>i. if i < n_ then i else Suc i)) z = ((\<lambda>i. if i < Suc n_ then i else Suc i) \<circ> Suc) z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
find_first x (insert_nth (Suc n_) x_ (y_ # ys_)) = map_option (\<lambda>i. if i < Suc n_ then i else Suc i) (find_first x (y_ # ys_))

goal (2 subgoals):
 1. \<And>xa xs. x \<noteq> xa \<Longrightarrow> find_first x (insert_nth 0 xa xs) = map_option (\<lambda>i. if i < 0 then i else Suc i) (find_first x xs)
 2. \<And>n xa. x \<noteq> xa \<Longrightarrow> find_first x (insert_nth (Suc n) xa []) = map_option (\<lambda>i. if i < Suc n then i else Suc i) (find_first x [])
[PROOF STEP]
qed auto


[STATEMENT]
lemma m1_obs_id [simp]: "obs m1 = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs m1 = id
[PROOF STEP]
by (simp add: m1_def)


[STATEMENT]
lemma PO_m1_inv0_fin_init [iff]:
  "init m1 \<subseteq> m1_inv0_fin"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m1 \<subseteq> m1_inv0_fin
[PROOF STEP]
by (auto simp add: m1_defs intro!: m1_inv0_finI)


[STATEMENT]
lemma PO_m1_inv0_fin_trans [iff]:
  "{m1_inv0_fin} trans m1 {> m1_inv0_fin}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m1_inv0_fin} TS.trans m1 {> m1_inv0_fin}
[PROOF STEP]
by (auto simp add: PO_hoare_defs m1_defs intro!: m1_inv0_finI)


[STATEMENT]
lemma PO_m1_inv0_fin [iff]: "reach m1 \<subseteq> m1_inv0_fin"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m1 \<subseteq> m1_inv0_fin
[PROOF STEP]
by (rule inv_rule_incr, auto del: subsetI)


[STATEMENT]
lemma knC_runs1a1 [simp]:
  "knC (runs1a1 runz) = knC runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. knC (runs1a1 runz) = knC runz
[PROOF STEP]
apply (auto simp add: map_runs_def elim!: knC.cases)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>Ra A B K al b. \<lbrakk>runz Ra = Some (Init, [A, B], b); take (Suc 0) b = aKey K # al\<rbrakk> \<Longrightarrow> (K, A) \<in> knC runz
 2. \<And>Rb A B K al b. \<lbrakk>runz Rb = Some (Resp, [A, B], b); take (Suc 0) b = aKey K # al\<rbrakk> \<Longrightarrow> (K, B) \<in> knC runz
 3. \<And>Rs. \<lbrakk>Rs \<in> dom runz; runz Rs = None; fst (the None) = Serv\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), Sv) \<in> knC runz
 4. \<And>Rs aa b. \<lbrakk>Rs \<in> dom runz; runz Rs = Some (Serv, aa, b)\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), Sv) \<in> knC runz
 5. \<And>Ra A B K al. runz Ra = Some (Init, [A, B], aKey K # al) \<Longrightarrow> (K, A) \<in> knC (runs1a1 runz)
 6. \<And>Rb A B K al. runz Rb = Some (Resp, [A, B], aKey K # al) \<Longrightarrow> (K, B) \<in> knC (runs1a1 runz)
 7. \<And>Rs. \<lbrakk>Rs \<in> dom runz; fst (the (runz Rs)) = Serv\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), Sv) \<in> knC (runs1a1 runz)
[PROOF STEP]
apply (rename_tac b, case_tac b, auto)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Rb A B K al b. \<lbrakk>runz Rb = Some (Resp, [A, B], b); take (Suc 0) b = aKey K # al\<rbrakk> \<Longrightarrow> (K, B) \<in> knC runz
 2. \<And>Ra A B K al. runz Ra = Some (Init, [A, B], aKey K # al) \<Longrightarrow> (K, A) \<in> knC (runs1a1 runz)
 3. \<And>Rb A B K al. runz Rb = Some (Resp, [A, B], aKey K # al) \<Longrightarrow> (K, B) \<in> knC (runs1a1 runz)
 4. \<And>Rs. \<lbrakk>Rs \<in> dom runz; fst (the (runz Rs)) = Serv\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), Sv) \<in> knC (runs1a1 runz)
[PROOF STEP]
apply (rename_tac b, case_tac b, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Ra A B K al. runz Ra = Some (Init, [A, B], aKey K # al) \<Longrightarrow> (K, A) \<in> knC (runs1a1 runz)
 2. \<And>Rb A B K al. runz Rb = Some (Resp, [A, B], aKey K # al) \<Longrightarrow> (K, B) \<in> knC (runs1a1 runz)
 3. \<And>Rs. \<lbrakk>Rs \<in> dom runz; fst (the (runz Rs)) = Serv\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), Sv) \<in> knC (runs1a1 runz)
[PROOF STEP]
apply (rule knC_init, auto simp add: runs1a1_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Rb A B K al. runz Rb = Some (Resp, [A, B], aKey K # al) \<Longrightarrow> (K, B) \<in> knC (runs1a1 runz)
 2. \<And>Rs. \<lbrakk>Rs \<in> dom runz; fst (the (runz Rs)) = Serv\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), Sv) \<in> knC (runs1a1 runz)
[PROOF STEP]
apply (rule knC_resp, auto simp add: runs1a1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rs. \<lbrakk>Rs \<in> dom runz; fst (the (runz Rs)) = Serv\<rbrakk> \<Longrightarrow> (sesK (Rs $ sk), Sv) \<in> knC (runs1a1 runz)
[PROOF STEP]
apply (rule_tac knC_serv, auto simp add: runs1a1_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_step1_refines_m1a_step1:
  "{R1a1}
     (m1a_step1 Ra A B Na), (m1_step1 Ra A B Na)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step1 Ra A B Na, m1_step1 Ra A B Na {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_step2_refines_m1a_step2:
  "{R1a1}
     (m1a_step2 Rb A B), (m1_step2 Rb A B)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step2 Rb A B, m1_step2 Rb A B {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_step3_refines_m1a_step3:
  "{R1a1}
     (m1a_step3 Rs A B Kab Na []), (m1_step3 Rs A B Na Kab)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step3 Rs A B Kab Na [], m1_step3 Rs A B Na Kab {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs)


[STATEMENT]
lemma PO_m1_step4_refines_m1a_step4:
  "{R1a1}
     (m1a_step4 Ra A B Na Kab []), (m1_step4 Ra A B Na Kab)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step4 Ra A B Na Kab [], m1_step4 Ra A B Na Kab {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs runs1a1_def)


[STATEMENT]
lemma PO_m1_step5_refines_m1a_step5:
  "{R1a1}
     (m1a_step5 Rb A B Kab []), (m1_step5 Rb A B Nb Kab)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_step5 Rb A B Kab [], m1_step5 Rb A B Nb Kab {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs runs1a1_def)


[STATEMENT]
lemma PO_m1_step6_refines_m1a_skip:
  "{R1a1}
     Id, (m1_step6 Ra A B Na Nb Kab)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} Id, m1_step6 Ra A B Na Nb Kab {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs runs1a1_def)


[STATEMENT]
lemma PO_m1_step7_refines_m1a_skip:
  "{R1a1}
     Id, (m1_step7 Rb A B Nb Kab)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} Id, m1_step7 Rb A B Nb Kab {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs runs1a1_def)


[STATEMENT]
lemma PO_m1_leak_refines_m1a_leak:
  "{R1a1}
     (m1a_leak Rs), (m1_leak Rs Ra Rb A B)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} m1a_leak Rs, m1_leak Rs Ra Rb A B {> R1a1}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R1a1_defs m1_defs map_runs_def dest: dom_lemmas)


[STATEMENT]
lemma PO_m1_refines_init_m1a [iff]:
  "init m1 \<subseteq>  R1a1``(init m1a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m1 \<subseteq> R1a1 `` init m1a
[PROOF STEP]
by (auto simp add: R1a1_defs m1a_defs m1_loc_defs)


[STATEMENT]
lemma PO_m1_refines_trans_m1a [iff]:
  "{R1a1}
     (trans m1a), (trans m1)
   {> R1a1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R1a1} TS.trans m1a, TS.trans m1 {> R1a1}
[PROOF STEP]
apply (auto simp add: m1_def m1_trans_def m1a_def m1a_trans_def
         intro!: PO_m1_trans_refines_m1a_trans)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa xb xe. {R1a1} (\<Union>x xa xb xc xd. (\<Union>xe xf. m1a_step1 xb x xa xe \<union> m1a_step2 xc x xa \<union> \<Union> (range (m1a_step3 xd x xa xf xe)) \<union> \<Union> (range (m1a_step4 xb x xa xe xf)) \<union> \<Union> (range (m1a_step5 xc x xa xf))) \<union> m1a_leak xd)\<^sup>=, m1_step1 xb x xa xe {> R1a1}
 2. \<And>x xa xc. {R1a1} (\<Union>x xa xb xc xd. (\<Union>xe xf. m1a_step1 xb x xa xe \<union> m1a_step2 xc x xa \<union> \<Union> (range (m1a_step3 xd x xa xf xe)) \<union> \<Union> (range (m1a_step4 xb x xa xe xf)) \<union> \<Union> (range (m1a_step5 xc x xa xf))) \<union> m1a_leak xd)\<^sup>=, m1_step2 xc x xa {> R1a1}
 3. \<And>x xa xd xe Kab. {R1a1} (\<Union>x xa xb xc xd. (\<Union>xe xf. m1a_step1 xb x xa xe \<union> m1a_step2 xc x xa \<union> \<Union> (range (m1a_step3 xd x xa xf xe)) \<union> \<Union> (range (m1a_step4 xb x xa xe xf)) \<union> \<Union> (range (m1a_step5 xc x xa xf))) \<union> m1a_leak xd)\<^sup>=, m1_step3 xd x xa xe Kab {> R1a1}
[PROOF STEP]
apply (force intro!: PO_m1_trans_refines_m1a_trans)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma obs_consistent_med1a1 [iff]:
  "obs_consistent R1a1 med1a1 m1a m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_consistent R1a1 med1a1 m1a m1
[PROOF STEP]
by (auto simp add: obs_consistent_def R1a1_def med1a1_def m1a_def m1_def)


[STATEMENT]
lemma PO_m1_refines_m1a [iff]:
  "refines R1a1 med1a1 m1a m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refines R1a1 med1a1 m1a m1
[PROOF STEP]
by (rule Refinement_basic) (auto del: subsetI)


[STATEMENT]
lemma  m1_implements_m1a [iff]: "implements med1a1 m1a m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. implements med1a1 m1a m1
[PROOF STEP]
by (rule refinement_soundness) (fast)


[STATEMENT]
lemma PO_m1_obs_secrecy [iff]: "oreach m1 \<subseteq> m1_secrecy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oreach m1 \<subseteq> m1_secrecy
[PROOF STEP]
apply (rule_tac Q=m1x_secrecy in external_invariant_translation)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. oreach ?Sa \<subseteq> m1x_secrecy
 2. ?pi -` m1x_secrecy \<subseteq> m1_secrecy
 3. implements ?pi ?Sa m1
[PROOF STEP]
apply (auto del: subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. med1a1 -` m1x_secrecy \<subseteq> m1_secrecy
[PROOF STEP]
apply (fastforce simp add: med1a1_def intro!: m1_secrecyI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_secrecy [iff]: "reach m1 \<subseteq> m1_secrecy"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m1 \<subseteq> m1_secrecy
[PROOF STEP]
by (rule external_to_internal_invariant) (auto del: subsetI)


[STATEMENT]
lemma PO_m1_inv2i_serv [iff]: "reach m1 \<subseteq> m1_inv2i_serv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m1 \<subseteq> m1_inv2i_serv
[PROOF STEP]
apply (rule_tac Pa=m1a_inv2i_serv and Qa=m1a_inv2i_serv and Q=m1_inv2i_serv
       in internal_invariant_translation)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. reach ?Sa \<subseteq> m1a_inv2i_serv
 2. m1a_inv2i_serv \<subseteq> obs ?Sa -` m1a_inv2i_serv
 3. ?pi -` m1a_inv2i_serv \<subseteq> m1_inv2i_serv
 4. obs m1 -` m1_inv2i_serv \<subseteq> m1_inv2i_serv
 5. implements ?pi ?Sa m1
[PROOF STEP]
apply (auto del: subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. med1a1 -` m1a_inv2i_serv \<subseteq> m1_inv2i_serv
[PROOF STEP]
apply (auto simp add: m1a_inv2i_serv_def med1a1_def vimage_def
            intro!: m1_inv2i_servI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x A B Ra Kab nla. \<lbrakk>A \<notin> bad; runs x Ra = Some (Init, [A, B], aKey Kab # nla); \<forall>A. A \<notin> bad \<longrightarrow> (\<forall>B Ra Kab. (\<exists>nla. runs1a1 (runs x) Ra = Some (Init, [A, B], aKey Kab # nla)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs1a1 (runs x) Rs = Some (Serv, [A, B], [aNon (Ra $ na)])))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs x Rs = Some (Serv, [A, B], [aNon (Ra $ na)])
[PROOF STEP]
apply (rename_tac s A B Ra Kab nla)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Ra Kab nla. \<lbrakk>A \<notin> bad; runs s Ra = Some (Init, [A, B], aKey Kab # nla); \<forall>A. A \<notin> bad \<longrightarrow> (\<forall>B Ra Kab. (\<exists>nla. runs1a1 (runs s) Ra = Some (Init, [A, B], aKey Kab # nla)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon (Ra $ na)])))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs s Rs = Some (Serv, [A, B], [aNon (Ra $ na)])
[PROOF STEP]
apply (drule_tac x=A in spec, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Ra Kab nla. \<lbrakk>A \<notin> bad; runs s Ra = Some (Init, [A, B], aKey Kab # nla); \<forall>B Ra Kab. (\<exists>nla. runs1a1 (runs s) Ra = Some (Init, [A, B], aKey Kab # nla)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon (Ra $ na)]))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs s Rs = Some (Serv, [A, B], [aNon (Ra $ na)])
[PROOF STEP]
apply (drule_tac x=B in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Ra Kab nla. \<lbrakk>A \<notin> bad; runs s Ra = Some (Init, [A, B], aKey Kab # nla); \<forall>Ra Kab. (\<exists>nla. runs1a1 (runs s) Ra = Some (Init, [A, B], aKey Kab # nla)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon (Ra $ na)]))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs s Rs = Some (Serv, [A, B], [aNon (Ra $ na)])
[PROOF STEP]
apply (drule_tac x=Ra in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Ra Kab nla. \<lbrakk>A \<notin> bad; runs s Ra = Some (Init, [A, B], aKey Kab # nla); \<forall>Kab. (\<exists>nla. runs1a1 (runs s) Ra = Some (Init, [A, B], aKey Kab # nla)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon (Ra $ na)]))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs s Rs = Some (Serv, [A, B], [aNon (Ra $ na)])
[PROOF STEP]
apply (drule_tac x=Kab in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Ra Kab nla. \<lbrakk>A \<notin> bad; runs s Ra = Some (Init, [A, B], aKey Kab # nla); (\<exists>nla. runs1a1 (runs s) Ra = Some (Init, [A, B], aKey Kab # nla)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon (Ra $ na)]))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> runs s Rs = Some (Serv, [A, B], [aNon (Ra $ na)])
[PROOF STEP]
apply (clarsimp simp add: runs1a1_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_inv2r_serv [iff]: "reach m1 \<subseteq> m1_inv2r_serv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m1 \<subseteq> m1_inv2r_serv
[PROOF STEP]
apply (rule_tac Pa=m1a_inv2r_serv and Qa=m1a_inv2r_serv and Q=m1_inv2r_serv
       in internal_invariant_translation)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. reach ?Sa \<subseteq> m1a_inv2r_serv
 2. m1a_inv2r_serv \<subseteq> obs ?Sa -` m1a_inv2r_serv
 3. ?pi -` m1a_inv2r_serv \<subseteq> m1_inv2r_serv
 4. obs m1 -` m1_inv2r_serv \<subseteq> m1_inv2r_serv
 5. implements ?pi ?Sa m1
[PROOF STEP]
apply (auto del: subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. med1a1 -` m1a_inv2r_serv \<subseteq> m1_inv2r_serv
[PROOF STEP]
apply (auto simp add: simp add: m1a_inv2r_serv_def med1a1_def vimage_def
            intro!: m1_inv2r_servI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x A B Rb Kab nlb. \<lbrakk>B \<notin> bad; runs x Rb = Some (Resp, [A, B], aKey Kab # nlb); \<forall>A B. B \<notin> bad \<longrightarrow> (\<forall>Rb Kab. (\<exists>nlb. runs1a1 (runs x) Rb = Some (Resp, [A, B], aKey Kab # nlb)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs1a1 (runs x) Rs = Some (Serv, [A, B], [aNon Na]))))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs x Rs = Some (Serv, [A, B], [aNon Na]))
[PROOF STEP]
apply (rename_tac s A B Rb Kab nlb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab nlb. \<lbrakk>B \<notin> bad; runs s Rb = Some (Resp, [A, B], aKey Kab # nlb); \<forall>A B. B \<notin> bad \<longrightarrow> (\<forall>Rb Kab. (\<exists>nlb. runs1a1 (runs s) Rb = Some (Resp, [A, B], aKey Kab # nlb)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon Na]))))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs s Rs = Some (Serv, [A, B], [aNon Na]))
[PROOF STEP]
apply (drule_tac x=A in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab nlb. \<lbrakk>B \<notin> bad; runs s Rb = Some (Resp, [A, B], aKey Kab # nlb); \<forall>B. B \<notin> bad \<longrightarrow> (\<forall>Rb Kab. (\<exists>nlb. runs1a1 (runs s) Rb = Some (Resp, [A, B], aKey Kab # nlb)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon Na]))))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs s Rs = Some (Serv, [A, B], [aNon Na]))
[PROOF STEP]
apply (drule_tac x=B in spec, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab nlb. \<lbrakk>B \<notin> bad; runs s Rb = Some (Resp, [A, B], aKey Kab # nlb); \<forall>Rb Kab. (\<exists>nlb. runs1a1 (runs s) Rb = Some (Resp, [A, B], aKey Kab # nlb)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon Na])))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs s Rs = Some (Serv, [A, B], [aNon Na]))
[PROOF STEP]
apply (drule_tac x=Rb in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab nlb. \<lbrakk>B \<notin> bad; runs s Rb = Some (Resp, [A, B], aKey Kab # nlb); \<forall>Kab. (\<exists>nlb. runs1a1 (runs s) Rb = Some (Resp, [A, B], aKey Kab # nlb)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon Na])))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs s Rs = Some (Serv, [A, B], [aNon Na]))
[PROOF STEP]
apply (drule_tac x=Kab in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab nlb. \<lbrakk>B \<notin> bad; runs s Rb = Some (Resp, [A, B], aKey Kab # nlb); (\<exists>nlb. runs1a1 (runs s) Rb = Some (Resp, [A, B], aKey Kab # nlb)) \<longrightarrow> (\<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs1a1 (runs s) Rs = Some (Serv, [A, B], [aNon Na])))\<rbrakk> \<Longrightarrow> \<exists>Rs. Kab = sesK (Rs $ sk) \<and> (\<exists>Na. runs s Rs = Some (Serv, [A, B], [aNon Na]))
[PROOF STEP]
apply (clarsimp simp add: runs1a1_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_inv3_ifresh [iff]: "reach m1 \<subseteq> m1_inv3_ifresh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m1 \<subseteq> m1_inv3_ifresh
[PROOF STEP]
apply (rule_tac Pa=m1a_inv1_ifresh and Qa=m1a_inv1_ifresh and Q=m1_inv3_ifresh
       in internal_invariant_translation)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. reach ?Sa \<subseteq> m1a_inv1_ifresh
 2. m1a_inv1_ifresh \<subseteq> obs ?Sa -` m1a_inv1_ifresh
 3. ?pi -` m1a_inv1_ifresh \<subseteq> m1_inv3_ifresh
 4. obs m1 -` m1_inv3_ifresh \<subseteq> m1_inv3_ifresh
 5. implements ?pi ?Sa m1
[PROOF STEP]
apply (auto del: subsetI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. med1a1 -` m1a_inv1_ifresh \<subseteq> m1_inv3_ifresh
[PROOF STEP]
apply (auto simp add: med1a1_def runs1a1_def vimage_def m1_inv3_ifresh_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ir_runs2sigs_empty [simp]:
   "runz = Map.empty \<Longrightarrow> ir_runs2sigs runz = (\<lambda>s. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runz = Map.empty \<Longrightarrow> ir_runs2sigs runz = (\<lambda>s. 0)
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ir_runs2sigs.induct, auto)


[STATEMENT]
lemma finite_ir_commit [simp, intro!]:
   "finite (dom runz) \<Longrightarrow> finite (ir_commit runz A B Kab Nb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom runz) \<Longrightarrow> finite (ir_commit runz A B Kab Nb)
[PROOF STEP]
by (auto intro: finite_subset dest: dom_lemmas)


[STATEMENT]
lemma ir_runs2sigs_upd_init_none [simp]:
  "\<lbrakk> Ra \<notin> dom runz \<rbrakk>
  \<Longrightarrow> ir_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], []))) = ir_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ra \<notin> dom runz \<Longrightarrow> ir_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], []))) = ir_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ir_runs2sigs.induct, auto dest: dom_lemmas)


[STATEMENT]
lemma ir_runs2sigs_upd_resp_none [simp]:
  "\<lbrakk> Rb \<notin> dom runz \<rbrakk>
  \<Longrightarrow> ir_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], []))) = ir_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rb \<notin> dom runz \<Longrightarrow> ir_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], []))) = ir_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ir_runs2sigs.induct, auto dest: dom_lemmas)


[STATEMENT]
lemma ir_runs2sigs_upd_serv_none [simp]:
  "\<lbrakk> Rs \<notin> dom runz \<rbrakk>
  \<Longrightarrow> ir_runs2sigs (runz(Rs \<mapsto> (Serv, [A, B], nl))) = ir_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rs \<notin> dom runz \<Longrightarrow> ir_runs2sigs (runz(Rs \<mapsto> (Serv, [A, B], nl))) = ir_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ir_runs2sigs.induct, auto dest: dom_lemmas)


[STATEMENT]
lemma ir_runs2sigs_upd_init_some [simp]:
  "\<lbrakk> runz Ra = Some (Init, [A, B], []) \<rbrakk>
  \<Longrightarrow> ir_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab]))) = ir_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runz Ra = Some (Init, [A, B], []) \<Longrightarrow> ir_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab]))) = ir_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ir_runs2sigs.induct, auto)


[STATEMENT]
lemma ir_runs2sigs_upd_init [simp]:
  "\<lbrakk> runz Ra = Some (Init, [A, B], [aKey Kab]); finite (dom runz) \<rbrakk>
  \<Longrightarrow> ir_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab, aNon Nb]))) =
     (ir_runs2sigs runz)
       (Commit [A, B] (Kab, Nb) := Suc (card (ir_commit runz A B Kab Nb)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>runz Ra = Some (Init, [A, B], [aKey Kab]); finite (dom runz)\<rbrakk> \<Longrightarrow> ir_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab, aNon Nb]))) = (ir_runs2sigs runz)(Commit [A, B] (Kab, Nb) := Suc (card (ir_commit runz A B Kab Nb)))
[PROOF STEP]
apply (rule ext, erule rev_mp, erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. finite (dom runz) \<longrightarrow> runz Ra = Some (Init, [A, B], [aKey Kab]) \<longrightarrow> ir_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab, aNon Nb]))) x = ((ir_runs2sigs runz)(Commit [A, B] (Kab, Nb) := Suc (card (ir_commit runz A B Kab Nb)))) x
[PROOF STEP]
apply (rule_tac ?a0.0=runz in ir_runs2sigs.induct, auto)
\<comment> \<open>1 subgoal, solved using @{thm "card_insert_disjoint"}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>runz. \<lbrakk>finite (dom runz); runz Ra = Some (Init, [A, B], [aKey Kab])\<rbrakk> \<Longrightarrow> card {Raa. Raa \<noteq> Ra \<longrightarrow> runz Raa = Some (Init, [A, B], [aKey Kab, aNon Nb])} = Suc (card (ir_commit runz A B Kab Nb))
[PROOF STEP]
apply (rename_tac runz)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>runz. \<lbrakk>finite (dom runz); runz Ra = Some (Init, [A, B], [aKey Kab])\<rbrakk> \<Longrightarrow> card {Raa. Raa \<noteq> Ra \<longrightarrow> runz Raa = Some (Init, [A, B], [aKey Kab, aNon Nb])} = Suc (card (ir_commit runz A B Kab Nb))
[PROOF STEP]
apply (rule_tac
         s="card (insert Ra (ir_commit runz A B Kab Nb))"
       in trans, fast, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ir_runs2sigs_upd_resp_some [simp]:
  "\<lbrakk> runz Rb = Some (Resp, [A, B], [aKey K]) \<rbrakk>
  \<Longrightarrow> ir_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey K, END]))) = ir_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runz Rb = Some (Resp, [A, B], [aKey K]) \<Longrightarrow> ir_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey K, END]))) = ir_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ir_runs2sigs.induct, fastforce+)


[STATEMENT]
lemma m1_inv2i_serv_lemma:
  "\<lbrakk> runs t Ra  = Some (Init, [A, B], [aKey Kab, aNon Nb]);
     runs t Ra' = Some (Init, [A, B], [aKey Kab]);
     A \<notin> bad; t \<in> m1_inv2i_serv \<rbrakk>
  \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>runs t Ra = Some (Init, [A, B], [aKey Kab, aNon Nb]); runs t Ra' = Some (Init, [A, B], [aKey Kab]); A \<notin> bad; t \<in> m1_inv2i_serv\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (frule m1_inv2i_servD, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rs. \<lbrakk>runs t Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb]); runs t Ra' = Some (Init, [A, B], [aKey (sesK (Rs $ sk))]); A \<notin> bad; t \<in> m1_inv2i_serv; runs t Rs = Some (Serv, [A, B], [aNon (Ra $ na)]); Kab = sesK (Rs $ sk)\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (rotate_tac 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rs. \<lbrakk>runs t Ra' = Some (Init, [A, B], [aKey (sesK (Rs $ sk))]); A \<notin> bad; t \<in> m1_inv2i_serv; runs t Rs = Some (Serv, [A, B], [aNon (Ra $ na)]); Kab = sesK (Rs $ sk); runs t Ra = Some (Init, [A, B], [aKey (sesK (Rs $ sk)), aNon Nb])\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (frule m1_inv2i_servD, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_step1_refines_ir_a0i_skip:
  "{R_a0im1_ir}
     Id, (m1_step1 Ra A B Na)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir} Id, m1_step1 Ra A B Na {> R_a0im1_ir}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ir_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step2_refines_ir_a0i_skip:
  "{R_a0im1_ir}
     Id, (m1_step2 Rb A B)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir} Id, m1_step2 Rb A B {> R_a0im1_ir}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ir_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step3_refines_ir_a0i_skip:
  "{R_a0im1_ir}
     Id, (m1_step3 Rs A B Na Kab)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir} Id, m1_step3 Rs A B Na Kab {> R_a0im1_ir}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ir_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step4_refines_ir_a0i_skip:
  "{R_a0im1_ir}
     Id, (m1_step4 Ra A B Na Kab)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir} Id, m1_step4 Ra A B Na Kab {> R_a0im1_ir}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ir_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step5_refines_ir_a0i_running:
  "{R_a0im1_ir}
     (a0i_running [A, B] (Kab, Nb)), (m1_step5 Rb A B Nb Kab)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir} a0i_running [A, B] (Kab, Nb), m1_step5 Rb A B Nb Kab {> R_a0im1_ir}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ir_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step6_refines_ir_a0i_commit:
  "{R_a0im1_ir \<inter> UNIV \<times> (m1_inv2i_serv \<inter> m1_inv0_fin)}
     (a0i_commit [A, B] (Kab, Nb)), (m1_step6 Ra A B Na Nb Kab)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir \<inter> UNIV \<times> (m1_inv2i_serv \<inter> m1_inv0_fin)} a0i_commit [A, B] (Kab, Nb), m1_step6 Ra A B Na Nb Kab {> R_a0im1_ir}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ir_defs a0i_defs m1_defs, safe, auto)
   (auto dest: m1_inv2i_serv_lemma)


[STATEMENT]
lemma PO_m1_step7_refines_ir_a0i_skip:
  "{R_a0im1_ir}
     Id, (m1_step7 Rb A B Nb Kab)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir} Id, m1_step7 Rb A B Nb Kab {> R_a0im1_ir}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ir_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_leak_refines_ir_a0i_corrupt:
  "{R_a0im1_ir}
     (a0i_corrupt ({sesK (Rs$sk)} \<times> UNIV)), (m1_leak Rs Ra Rb A B)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir} a0i_corrupt ({sesK (Rs $ sk)} \<times> UNIV), m1_leak Rs Ra Rb A B {> R_a0im1_ir}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ir_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_refines_ir_init_a0i [iff]:
  "init m1 \<subseteq>  R_a0im1_ir``(init a0i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m1 \<subseteq> R_a0im1_ir `` init a0i
[PROOF STEP]
by (auto simp add: R_a0im1_ir_defs a0i_defs m1_defs
         intro!: exI [where x="\<lparr>signals = \<lambda>s. 0, corrupted = corrKey \<times> UNIV \<rparr>"])


[STATEMENT]
lemma PO_m1_refines_ir_trans_a0i [iff]:
  "{R_a0im1_ir \<inter> reach a0i \<times> reach m1}
     (trans a0i), (trans m1)
   {> R_a0im1_ir}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir \<inter> reach a0i \<times> reach m1} TS.trans a0i, TS.trans m1 {> R_a0im1_ir}
[PROOF STEP]
apply (rule_tac pre'="R_a0im1_ir \<inter> UNIV \<times> (m1_inv2i_serv \<inter> m1_inv0_fin)"
       in relhoare_conseq_left, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ir \<inter> UNIV \<times> (m1_inv2i_serv \<inter> m1_inv0_fin)} TS.trans a0i, TS.trans m1 {> R_a0im1_ir}
[PROOF STEP]
apply (auto simp add: m1_def m1_trans_def a0i_def a0i_trans_def
            intro!: PO_m1_trans_refines_ir_a0i_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma obs_consistent_med_a0im1_ir [iff]:
  "obs_consistent R_a0im1_ir med_a0im1_ir a0i m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_consistent R_a0im1_ir med_a0im1_ir a0i m1
[PROOF STEP]
by (auto simp add: obs_consistent_def R_a0im1_ir_def med_a0im1_ir_def
         a0i_def m1_def)


[STATEMENT]
lemma PO_m1_refines_ir_a0i [iff]:
  "refines
     (R_a0im1_ir \<inter> reach a0i \<times> reach m1)
     med_a0im1_ir a0i m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refines (R_a0im1_ir \<inter> reach a0i \<times> reach m1) med_a0im1_ir a0i m1
[PROOF STEP]
by (rule Refinement_using_invariants) (auto)


[STATEMENT]
lemma  m1_implements_ir_a0i: "implements med_a0im1_ir a0i m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. implements med_a0im1_ir a0i m1
[PROOF STEP]
by (rule refinement_soundness) (fast)


[STATEMENT]
lemma ri_runs2sigs_empty [simp]:
  "runz = Map.empty \<Longrightarrow> ri_runs2sigs runz = (\<lambda>s. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runz = Map.empty \<Longrightarrow> ri_runs2sigs runz = (\<lambda>s. 0)
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ri_runs2sigs.induct, auto)


[STATEMENT]
lemma finite_inv_ri_running [simp, intro!]:
   "finite (dom runz) \<Longrightarrow> finite (ri_running runz A B Kab Nb)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom runz) \<Longrightarrow> finite (ri_running runz A B Kab Nb)
[PROOF STEP]
by (auto intro: finite_subset dest: dom_lemmas)


[STATEMENT]
lemma ri_runs2sigs_upd_init_none [simp]:
  "\<lbrakk> Na \<notin> dom runz \<rbrakk>
  \<Longrightarrow> ri_runs2sigs (runz(Na \<mapsto> (Init, [A, B], []))) = ri_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Na \<notin> dom runz \<Longrightarrow> ri_runs2sigs (runz(Na \<mapsto> (Init, [A, B], []))) = ri_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ri_runs2sigs.induct, auto dest: dom_lemmas)


[STATEMENT]
lemma ri_runs2sigs_upd_resp_none [simp]:
  "\<lbrakk> Rb \<notin> dom runz \<rbrakk>
  \<Longrightarrow> ri_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], []))) = ri_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rb \<notin> dom runz \<Longrightarrow> ri_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], []))) = ri_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ri_runs2sigs.induct, auto dest: dom_lemmas)


[STATEMENT]
lemma ri_runs2sigs_upd_serv_none [simp]:
  "\<lbrakk> Rs \<notin> dom runz \<rbrakk>
  \<Longrightarrow> ri_runs2sigs (runz(Rs \<mapsto> (Serv, [A, B], nl))) = ri_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rs \<notin> dom runz \<Longrightarrow> ri_runs2sigs (runz(Rs \<mapsto> (Serv, [A, B], nl))) = ri_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ri_runs2sigs.induct, auto dest: dom_lemmas)


[STATEMENT]
lemma ri_runs2sigs_upd_init [simp]:
  "\<lbrakk> runz Ra = Some (Init, [A, B], [aKey Kab]); finite (dom runz) \<rbrakk>
  \<Longrightarrow> ri_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab, aNon Nb]))) =
     (ri_runs2sigs runz)
       (Running [B, A] (Kab, Nb) := Suc (card (ri_running runz A B Kab Nb)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>runz Ra = Some (Init, [A, B], [aKey Kab]); finite (dom runz)\<rbrakk> \<Longrightarrow> ri_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab, aNon Nb]))) = (ri_runs2sigs runz)(Running [B, A] (Kab, Nb) := Suc (card (ri_running runz A B Kab Nb)))
[PROOF STEP]
apply (rule ext, erule rev_mp, erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. finite (dom runz) \<longrightarrow> runz Ra = Some (Init, [A, B], [aKey Kab]) \<longrightarrow> ri_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab, aNon Nb]))) x = ((ri_runs2sigs runz)(Running [B, A] (Kab, Nb) := Suc (card (ri_running runz A B Kab Nb)))) x
[PROOF STEP]
apply (rule_tac ?a0.0=runz in ri_runs2sigs.induct, auto)
\<comment> \<open>1 subgoal, solved using @{thm "card_insert_disjoint"}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>runz. \<lbrakk>finite (dom runz); runz Ra = Some (Init, [A, B], [aKey Kab])\<rbrakk> \<Longrightarrow> card {Raa. Raa \<noteq> Ra \<longrightarrow> runz Raa = Some (Init, [A, B], [aKey Kab, aNon Nb])} = Suc (card (ri_running runz A B Kab Nb))
[PROOF STEP]
apply (rename_tac runz)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>runz. \<lbrakk>finite (dom runz); runz Ra = Some (Init, [A, B], [aKey Kab])\<rbrakk> \<Longrightarrow> card {Raa. Raa \<noteq> Ra \<longrightarrow> runz Raa = Some (Init, [A, B], [aKey Kab, aNon Nb])} = Suc (card (ri_running runz A B Kab Nb))
[PROOF STEP]
apply (rule_tac
         s="card (insert Ra (ri_running runz A B Kab Nb))"
       in trans, fast, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ri_runs2sigs_upd_init_some [simp]:
  "\<lbrakk> runz Ra = Some (Init, [A, B], []) \<rbrakk>
  \<Longrightarrow> ri_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab]))) = ri_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runz Ra = Some (Init, [A, B], []) \<Longrightarrow> ri_runs2sigs (runz(Ra \<mapsto> (Init, [A, B], [aKey Kab]))) = ri_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ri_runs2sigs.induct, auto)


[STATEMENT]
lemma ri_runs2sigs_upd_resp_some [simp]:
  "\<lbrakk> runz Rb = Some (Resp, [A, B], [])\<rbrakk>
  \<Longrightarrow> ri_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey K]))) = ri_runs2sigs runz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runz Rb = Some (Resp, [A, B], []) \<Longrightarrow> ri_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey K]))) = ri_runs2sigs runz
[PROOF STEP]
by (rule ext, erule rev_mp)
   (rule ri_runs2sigs.induct, auto)


[STATEMENT]
lemma ri_runs2sigs_upd_resp_some2 [simp]:
  "\<lbrakk> runz Rb = Some (Resp, [A, B], [aKey Kab]) \<rbrakk>
  \<Longrightarrow> ri_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey Kab, END]))) =
     (ri_runs2sigs runz)(Commit [B, A] (Kab, Rb$nb) := 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runz Rb = Some (Resp, [A, B], [aKey Kab]) \<Longrightarrow> ri_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey Kab, END]))) = (ri_runs2sigs runz)(Commit [B, A] (Kab, Rb $ nb) := 1)
[PROOF STEP]
apply (rule ext, erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. runz Rb = Some (Resp, [A, B], [aKey Kab]) \<longrightarrow> ri_runs2sigs (runz(Rb \<mapsto> (Resp, [A, B], [aKey Kab, END]))) x = ((ri_runs2sigs runz)(Commit [B, A] (Kab, Rb $ nb) := 1)) x
[PROOF STEP]
apply (rule ri_runs2sigs.induct, fastforce+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_step1_refines_ri_a0i_skip:
  "{R_a0im1_ri}
     Id, (m1_step1 Ra A B Na)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri} Id, m1_step1 Ra A B Na {> R_a0im1_ri}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ri_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step2_refines_ri_a0i_skip:
  "{R_a0im1_ri}
     Id, (m1_step2 Rb A B)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri} Id, m1_step2 Rb A B {> R_a0im1_ri}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ri_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step3_refines_ri_a0i_skip:
  "{R_a0im1_ri}
     Id, (m1_step3 Rs A B Na Kab)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri} Id, m1_step3 Rs A B Na Kab {> R_a0im1_ri}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ri_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step4_refines_ri_a0i_skip:
  "{R_a0im1_ri}
     Id, (m1_step4 Ra A B Nb Kab)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri} Id, m1_step4 Ra A B Nb Kab {> R_a0im1_ri}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ri_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step5_refines_ri_a0i_skip:
  "{R_a0im1_ri}
     Id, (m1_step5 Rb A B Nb Kab)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri} Id, m1_step5 Rb A B Nb Kab {> R_a0im1_ri}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ri_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step6_refines_ri_a0i_running:
  "{R_a0im1_ri \<inter> UNIV \<times> m1_inv0_fin}
     (a0i_running [B, A] (Kab, Nb)), (m1_step6 Ra A B Na Nb Kab)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri \<inter> UNIV \<times> m1_inv0_fin} a0i_running [B, A] (Kab, Nb), m1_step6 Ra A B Na Nb Kab {> R_a0im1_ri}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ri_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_step7_refines_ri_a0i_commit:
  "{R_a0im1_ri \<inter> UNIV \<times> m1_inv0_fin}
     (a0i_commit [B, A] (Kab, Nb)), (m1_step7 Rb A B Nb Kab)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri \<inter> UNIV \<times> m1_inv0_fin} a0i_commit [B, A] (Kab, Nb), m1_step7 Rb A B Nb Kab {> R_a0im1_ri}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ri_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_leak_refines_ri_a0i_corrupt:
  "{R_a0im1_ri}
     (a0i_corrupt ({sesK (Rs$sk)} \<times> UNIV)), (m1_leak Rs Ra Rb A B)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri} a0i_corrupt ({sesK (Rs $ sk)} \<times> UNIV), m1_leak Rs Ra Rb A B {> R_a0im1_ri}
[PROOF STEP]
by (simp add: PO_rhoare_defs R_a0im1_ri_defs a0i_defs m1_defs, safe, auto)


[STATEMENT]
lemma PO_m1_refines_ri_init_a0i [iff]:
  "init m1 \<subseteq>  R_a0im1_ri``(init a0i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m1 \<subseteq> R_a0im1_ri `` init a0i
[PROOF STEP]
by (auto simp add: R_a0im1_ri_defs a0i_defs m1_defs
         intro!: exI [where x="\<lparr>signals = \<lambda>s. 0, corrupted = corrKey \<times> UNIV \<rparr>"])


[STATEMENT]
lemma PO_m1_refines_ri_trans_a0i [iff]:
  "{R_a0im1_ri \<inter> a0i_inv1_iagree \<times> m1_inv0_fin}
     (trans a0i), (trans m1)
   {> R_a0im1_ri}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R_a0im1_ri \<inter> a0i_inv1_iagree \<times> m1_inv0_fin} TS.trans a0i, TS.trans m1 {> R_a0im1_ri}
[PROOF STEP]
by (auto simp add: m1_def m1_trans_def a0i_def a0i_trans_def)
   (blast intro!: PO_m1_trans_refines_ri_a0i_trans)+


[STATEMENT]
lemma obs_consistent_med_a0im1_ri [iff]:
  "obs_consistent R_a0im1_ri med_a0im1_ri a0i m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obs_consistent R_a0im1_ri med_a0im1_ri a0i m1
[PROOF STEP]
by (auto simp add: obs_consistent_def R_a0im1_ri_def med_a0im1_ri_def a0i_def m1_def)


[STATEMENT]
lemma PO_m1_refines_ri_a0i [iff]:
  "refines (R_a0im1_ri \<inter> a0i_inv1_iagree \<times> m1_inv0_fin) med_a0im1_ri a0i m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refines (R_a0im1_ri \<inter> a0i_inv1_iagree \<times> m1_inv0_fin) med_a0im1_ri a0i m1
[PROOF STEP]
by (rule Refinement_using_invariants) (auto)


[STATEMENT]
lemma  m1_implements_ri_a0i: "implements med_a0im1_ri a0i m1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. implements med_a0im1_ri a0i m1
[PROOF STEP]
by (rule refinement_soundness) (fast)


[STATEMENT]
lemma PO_m1_inv3r_init [iff]: "reach m1 \<subseteq> m1_inv3r_init"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach m1 \<subseteq> m1_inv3r_init
[PROOF STEP]
apply (rule INV_from_Refinement_basic [OF PO_m1_refines_ri_a0i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Range (R_a0im1_ri \<inter> a0i_inv1_iagree \<times> m1_inv0_fin) \<subseteq> m1_inv3r_init
[PROOF STEP]
apply (auto simp add: R_a0im1_ri_def a0i_inv1_iagree_def
            intro!:  m1_inv3r_initI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x A B Rb Kab a. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak x); runs x Rb = Some (Resp, [A, B], [aKey Kab, END]); x \<in> m1_inv0_fin; \<forall>h. set h \<subseteq> good \<longrightarrow> (\<forall>a. a \<notin> Domain (m1_state.leak x) \<longrightarrow> (\<forall>b. ri_runs2sigs (runs x) (Commit h (a, b)) \<le> ri_runs2sigs (runs x) (Running h (a, b)))); signals a = ri_runs2sigs (runs x); corrupted a = Domain (m1_state.leak x) \<times> UNIV\<rbrakk> \<Longrightarrow> \<exists>Ra nla. runs x Ra = Some (Init, [A, B], aKey Kab # aNon (Rb $ nb) # nla)
[PROOF STEP]
apply (rename_tac s A B Rb Kab a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab a. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak s); runs s Rb = Some (Resp, [A, B], [aKey Kab, END]); s \<in> m1_inv0_fin; \<forall>h. set h \<subseteq> good \<longrightarrow> (\<forall>a. a \<notin> Domain (m1_state.leak s) \<longrightarrow> (\<forall>b. ri_runs2sigs (runs s) (Commit h (a, b)) \<le> ri_runs2sigs (runs s) (Running h (a, b)))); signals a = ri_runs2sigs (runs s); corrupted a = Domain (m1_state.leak s) \<times> UNIV\<rbrakk> \<Longrightarrow> \<exists>Ra nla. runs s Ra = Some (Init, [A, B], aKey Kab # aNon (Rb $ nb) # nla)
[PROOF STEP]
apply (drule_tac x="[B, A]" in spec, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab a. \<lbrakk>\<forall>a. a \<notin> Domain (m1_state.leak s) \<longrightarrow> (\<forall>b. (\<forall>Rb. b = Rb $ nb \<longrightarrow> runs s Rb \<noteq> Some (Resp, [A, B], [aKey a, END])) \<or> Suc 0 \<le> card (ri_running (runs s) A B a b)); B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak s); runs s Rb = Some (Resp, [A, B], [aKey Kab, END]); s \<in> m1_inv0_fin; signals a = ri_runs2sigs (runs s); corrupted a = Domain (m1_state.leak s) \<times> UNIV\<rbrakk> \<Longrightarrow> \<exists>Ra nla. runs s Ra = Some (Init, [A, B], aKey Kab # aNon (Rb $ nb) # nla)
[PROOF STEP]
apply (drule_tac x="Kab" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab a. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak s); runs s Rb = Some (Resp, [A, B], [aKey Kab, END]); s \<in> m1_inv0_fin; signals a = ri_runs2sigs (runs s); corrupted a = Domain (m1_state.leak s) \<times> UNIV; Kab \<notin> Domain (m1_state.leak s) \<longrightarrow> (\<forall>b. (\<forall>Rb. b = Rb $ nb \<longrightarrow> runs s Rb \<noteq> Some (Resp, [A, B], [aKey Kab, END])) \<or> Suc 0 \<le> card (ri_running (runs s) A B Kab b))\<rbrakk> \<Longrightarrow> \<exists>Ra nla. runs s Ra = Some (Init, [A, B], aKey Kab # aNon (Rb $ nb) # nla)
[PROOF STEP]
(* apply (drule_tac x="Rb$nb" in spec, auto) *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s A B Rb Kab a. \<lbrakk>B \<notin> bad; A \<notin> bad; Kab \<notin> Domain (m1_state.leak s); runs s Rb = Some (Resp, [A, B], [aKey Kab, END]); s \<in> m1_inv0_fin; signals a = ri_runs2sigs (runs s); corrupted a = Domain (m1_state.leak s) \<times> UNIV; Kab \<notin> Domain (m1_state.leak s) \<longrightarrow> (\<forall>b. (\<forall>Rb. b = Rb $ nb \<longrightarrow> runs s Rb \<noteq> Some (Resp, [A, B], [aKey Kab, END])) \<or> Suc 0 \<le> card (ri_running (runs s) A B Kab b))\<rbrakk> \<Longrightarrow> \<exists>Ra nla. runs s Ra = Some (Init, [A, B], aKey Kab # aNon (Rb $ nb) # nla)
[PROOF STEP]
apply (subgoal_tac "card (ri_running (runs s) A B Kab (Rb$nb)) > 0", auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma PO_m1_inv4_rfresh_init [iff]:
  "init m1 \<subseteq> m1_inv4_rfresh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init m1 \<subseteq> m1_inv4_rfresh
[PROOF STEP]
by (auto simp add: m1_defs intro!: m1_inv4_rfreshI)