[STATEMENT]
lemma node_ptr_kinds_M_reads:
  "reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) node_ptr_kinds_M h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reads (\<Union>object_ptr. {preserved (get_M object_ptr RObject.nothing)}) node_ptr_kinds_M h h'
[PROOF STEP]
using object_ptr_kinds_M_reads
[PROOF STATE]
proof (prove)
using this:
reads (\<Union>object_ptr. {preserved (get_M object_ptr RObject.nothing)}) object_ptr_kinds_M ?h ?h'

goal (1 subgoal):
 1. reads (\<Union>object_ptr. {preserved (get_M object_ptr RObject.nothing)}) node_ptr_kinds_M h h'
[PROOF STEP]
apply (simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
      object_ptr_kinds_M_reads preserved_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h h'. (\<forall>y. h \<turnstile> get_M y RObject.nothing \<rightarrow>\<^sub>r () = h' \<turnstile> get_M y RObject.nothing \<rightarrow>\<^sub>r ()) \<longrightarrow> (\<forall>x. (x = sorted_list_of_set (fset (object_ptr_kinds h))) = (x = sorted_list_of_set (fset (object_ptr_kinds h'))))) \<Longrightarrow> (\<forall>y. h \<turnstile> get_M y RObject.nothing \<rightarrow>\<^sub>r () = h' \<turnstile> get_M y RObject.nothing \<rightarrow>\<^sub>r ()) \<longrightarrow> (\<forall>x. (sorted_list_of_set ((\<lambda>x. the (cast x)) ` (Collect is_node_ptr_kind \<inter> fset (object_ptr_kinds h))) = x) = (sorted_list_of_set ((\<lambda>x. the (cast x)) ` (Collect is_node_ptr_kind \<inter> fset (object_ptr_kinds h'))) = x))
[PROOF STEP]
by (metis (mono_tags, lifting) object_ptr_kinds_preserved_small old.unit.exhaust preserved_def)


[STATEMENT]
lemma get_M_Object_preserved1 [simp]:
  "(\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)) \<Longrightarrow> h \<turnstile> put_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr setter v \<rightarrow>\<^sub>h h'
    \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
apply(cases "cast node_ptr = object_ptr")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; cast node_ptr = object_ptr\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
 2. \<lbrakk>\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; cast node_ptr \<noteq> object_ptr\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
by(auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def preserved_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def
      bind_eq_Some_conv
      split: option.splits)


[STATEMENT]
lemma get_M_Object_preserved2 [simp]:
  "cast node_ptr \<noteq> object_ptr \<Longrightarrow> h \<turnstile> put_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr setter v \<rightarrow>\<^sub>h h'
    \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cast node_ptr \<noteq> object_ptr; h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
by(auto simp add: put_M_defs get_M_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def ObjectMonad.get_M_defs preserved_def
      split: option.splits dest: get_heap_E)


[STATEMENT]
lemma get_M_Object_preserved3 [simp]:
  "h \<turnstile> put_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow> (\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x))
    \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
apply(cases "cast node_ptr \<noteq> object_ptr")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); cast node_ptr \<noteq> object_ptr\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
 2. \<lbrakk>h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); \<not> cast node_ptr \<noteq> object_ptr\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
by(auto simp add: put_M_defs get_M_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def ObjectMonad.get_M_defs preserved_def
      split: option.splits bind_splits dest: get_heap_E)


[STATEMENT]
lemma get_M_Object_preserved4 [simp]:
  "cast node_ptr \<noteq> object_ptr \<Longrightarrow> h \<turnstile> put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr setter v \<rightarrow>\<^sub>h h'
      \<Longrightarrow> preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cast node_ptr \<noteq> object_ptr; h \<turnstile> put_M object_ptr setter v \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> preserved (get_M node_ptr getter) h h'
[PROOF STEP]
by(auto simp add: ObjectMonad.put_M_defs get_M_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def ObjectMonad.get_M_defs preserved_def
      split: option.splits dest: get_heap_E)


[STATEMENT]
lemma get_node_ptr_simp [simp]:
  "get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) = (if ptr = cast node_ptr then cast obj else get node_ptr h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get node_ptr (put ptr obj h) = (if ptr = cast node_ptr then cast obj else get node_ptr h)
[PROOF STEP]
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)


[STATEMENT]
lemma node_ptr_kinds_simp [simp]:
  "node_ptr_kinds (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)
                = node_ptr_kinds h |\<union>| (if is_node_ptr_kind ptr then {|the (cast ptr)|} else {||})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. node_ptr_kinds (put ptr obj h) = node_ptr_kinds h |\<union>| (if is_node_ptr_kind ptr then {|the (cast ptr)|} else {||})
[PROOF STEP]
by(auto simp add: node_ptr_kinds_def)


[STATEMENT]
lemma type_wf_put_I:
  assumes "type_wf h"
  assumes "ObjectClass.type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
  assumes "is_node_ptr_kind ptr \<Longrightarrow> is_node_kind obj"
  shows "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf (put ptr obj h)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
NodeClass.type_wf h
ObjectClass.type_wf (put ptr obj h)
is_node_ptr_kind ptr \<Longrightarrow> is_node_kind obj

goal (1 subgoal):
 1. NodeClass.type_wf (put ptr obj h)
[PROOF STEP]
apply(auto simp add: type_wf_defs split: option.splits)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ObjectClass.type_wf (put ptr obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; is_node_ptr_kind ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
 2. \<And>node_ptr. \<lbrakk>ObjectClass.type_wf (put (cast node_ptr) obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h; ptr = cast node_ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
[PROOF STEP]
using cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none is_node_kind_def
[PROOF STATE]
proof (prove)
using this:
(cast ?obj = None) = (\<nexists>node. cast node = ?obj)
is_node_kind ?ptr = (cast ?ptr \<noteq> None)

goal (2 subgoals):
 1. \<lbrakk>ObjectClass.type_wf (put ptr obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; is_node_ptr_kind ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
 2. \<And>node_ptr. \<lbrakk>ObjectClass.type_wf (put (cast node_ptr) obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h; ptr = cast node_ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>node_ptr. \<lbrakk>ObjectClass.type_wf (put (cast node_ptr) obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h; ptr = cast node_ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
[PROOF STEP]
using cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none is_node_kind_def
[PROOF STATE]
proof (prove)
using this:
(cast ?obj = None) = (\<nexists>node. cast node = ?obj)
is_node_kind ?ptr = (cast ?ptr \<noteq> None)

goal (1 subgoal):
 1. \<And>node_ptr. \<lbrakk>ObjectClass.type_wf (put (cast node_ptr) obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h; ptr = cast node_ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
  assumes "ptr |\<notin>| object_ptr_kinds h"
  shows "type_wf h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
NodeClass.type_wf (put ptr obj h)
ptr |\<notin>| object_ptr_kinds h

goal (1 subgoal):
 1. NodeClass.type_wf h
[PROOF STEP]
by(auto simp add: type_wf_defs elim!: ObjectMonad.type_wf_put_ptr_not_in_heap_E
      split: option.splits if_splits)


[STATEMENT]
lemma node_ptr_kinds_small:
  assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
  shows "node_ptr_kinds h = node_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. node_ptr_kinds h = node_ptr_kinds h'
[PROOF STEP]
by(simp add: node_ptr_kinds_def preserved_def object_ptr_kinds_preserved_small[OF assms])


[STATEMENT]
lemma type_wf_preserved_small:
  assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
  assumes "\<And>node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'"
  shows "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
using type_wf_preserved allI[OF assms(2), of id, simplified]
[PROOF STATE]
proof (prove)
using this:
ObjectClass.type_wf ?h = ObjectClass.type_wf ?h'
\<forall>x. preserved (get_M x RNode.nothing) h h'

goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
apply(auto simp add: type_wf_defs)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>node_ptr. \<lbrakk>\<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'; \<forall>x. preserved (get_M x RNode.nothing) h h'; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h'\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h' = Some y
 2. \<And>node_ptr. \<lbrakk>\<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'; \<forall>x. preserved (get_M x RNode.nothing) h h'; ObjectClass.type_wf h'; \<forall>node_ptr\<in>fset (node_ptr_kinds h'). \<exists>y. get node_ptr h' = Some y; node_ptr |\<in>| node_ptr_kinds h\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h = Some y
[PROOF STEP]
apply(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)]
      split: option.splits)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>node_ptr. \<lbrakk>\<forall>x. ((\<exists>y. get x h = Some y) \<or> get x h' = None) \<and> (get x h = None \<or> (\<exists>y. get x h' = Some y)); ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h'). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h'; \<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h' = Some y
 2. \<And>node_ptr. \<lbrakk>\<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'; \<forall>x. preserved (get_M x RNode.nothing) h h'; ObjectClass.type_wf h'; \<forall>node_ptr\<in>fset (node_ptr_kinds h'). \<exists>y. get node_ptr h' = Some y; node_ptr |\<in>| node_ptr_kinds h\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h = Some y
[PROOF STEP]
apply (metis notin_fset option.simps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>node_ptr. \<lbrakk>\<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'; \<forall>x. preserved (get_M x RNode.nothing) h h'; ObjectClass.type_wf h'; \<forall>node_ptr\<in>fset (node_ptr_kinds h'). \<exists>y. get node_ptr h' = Some y; node_ptr |\<in>| node_ptr_kinds h\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h = Some y
[PROOF STEP]
by(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)]
      split: option.splits, force)[1]


[STATEMENT]
lemma type_wf_preserved:
  assumes "writes SW setter h h'"
  assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
  assumes "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h'
           \<Longrightarrow> \<forall>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
  assumes "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h'
           \<Longrightarrow> \<forall>node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'"
  shows "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
have "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
using assms type_wf_preserved_small
[PROOF STATE]
proof (prove)
using this:
writes SW setter h h'
h \<turnstile> setter \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> \<forall>object_ptr. preserved (get_M object_ptr RObject.nothing) ?h ?h'
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> \<forall>node_ptr. preserved (get_M node_ptr RNode.nothing) ?h ?h'
\<lbrakk>\<And>object_ptr. preserved (get_M object_ptr RObject.nothing) ?h ?h'; \<And>node_ptr. preserved (get_M node_ptr RNode.nothing) ?h ?h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf ?h = NodeClass.type_wf ?h'

goal (1 subgoal):
 1. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf ?h = NodeClass.type_wf ?h'

goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
with assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
writes SW setter h h'
h \<turnstile> setter \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf ?h = NodeClass.type_wf ?h'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
writes SW setter h h'
h \<turnstile> setter \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf ?h = NodeClass.type_wf ?h'

goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
apply(rule writes_small_big)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> ?w1 h h' w \<in> SW
 2. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> h \<turnstile> ?w1 h h' w \<rightarrow>\<^sub>h h'
 3. reflp (\<lambda>h h'. NodeClass.type_wf h = NodeClass.type_wf h')
 4. transp (\<lambda>h h'. NodeClass.type_wf h = NodeClass.type_wf h')
[PROOF STEP]
by(auto simp add: reflp_def transp_def)
[PROOF STATE]
proof (state)
this:
NodeClass.type_wf h = NodeClass.type_wf h'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma True_simps:
  "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
  "(PROP P \<Longrightarrow> True) \<equiv> PROP Trueprop True"
  "(\<And>x. True) \<equiv> PROP Trueprop True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((True \<Longrightarrow> PROP P) \<equiv> PROP P) &&& ((PROP P \<Longrightarrow> True) \<equiv> True) &&& (\<And>x. True) \<equiv> True
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (True \<Longrightarrow> PROP P) \<equiv> PROP P
 2. (PROP P \<Longrightarrow> True) \<equiv> True
 3. (\<And>x. True) \<equiv> True
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (True \<Longrightarrow> PROP P) \<Longrightarrow> PROP P
 2. \<lbrakk>PROP P; True\<rbrakk> \<Longrightarrow> PROP P
 3. (PROP P \<Longrightarrow> True) \<equiv> True
 4. (\<And>x. True) \<equiv> True
[PROOF STEP]
apply (erule meta_mp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. True
 2. \<lbrakk>PROP P; True\<rbrakk> \<Longrightarrow> PROP P
 3. (PROP P \<Longrightarrow> True) \<equiv> True
 4. (\<And>x. True) \<equiv> True
[PROOF STEP]
apply (rule TrueI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>PROP P; True\<rbrakk> \<Longrightarrow> PROP P
 2. (PROP P \<Longrightarrow> True) \<equiv> True
 3. (\<And>x. True) \<equiv> True
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (PROP P \<Longrightarrow> True) \<equiv> True
 2. (\<And>x. True) \<equiv> True
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (PROP P \<Longrightarrow> True) \<Longrightarrow> True
 2. \<lbrakk>True; PROP P\<rbrakk> \<Longrightarrow> True
 3. (\<And>x. True) \<equiv> True
[PROOF STEP]
apply (rule TrueI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>True; PROP P\<rbrakk> \<Longrightarrow> True
 2. (\<And>x. True) \<equiv> True
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. True) \<equiv> True
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>x. True) \<Longrightarrow> True
 2. \<And>x. True \<Longrightarrow> True
[PROOF STEP]
apply (rule TrueI)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ballpI: "(\<And>x y. (x, y) \<in> A \<Longrightarrow> P x y) \<Longrightarrow> \<forall>(x, y) \<in> A. P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. (x, y) \<in> A \<Longrightarrow> P x y) \<Longrightarrow> \<forall>(x, y)\<in>A. P x y
[PROOF STEP]
by blast


[STATEMENT]
lemma bpspec: "\<forall>(x, y) \<in> A. P x y \<Longrightarrow> (x, y) \<in> A \<Longrightarrow> P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>(x, y)\<in>A. P x y; (x, y) \<in> A\<rbrakk> \<Longrightarrow> P x y
[PROOF STEP]
by blast


[STATEMENT]
lemma ballpE: "\<forall>(x, y) \<in> A. P x y \<Longrightarrow> (P x y \<Longrightarrow> Q) \<Longrightarrow>
  ((x, y) \<notin> A \<Longrightarrow> Q) \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>(x, y)\<in>A. P x y; P x y \<Longrightarrow> Q; (x, y) \<notin> A \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
by blast


[STATEMENT]
lemma bexpI: "P x y \<Longrightarrow> (x, y) \<in> A \<Longrightarrow> \<exists>(x, y) \<in> A. P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P x y; (x, y) \<in> A\<rbrakk> \<Longrightarrow> \<exists>(x, y)\<in>A. P x y
[PROOF STEP]
by blast


[STATEMENT]
lemma bexpE: "\<exists>(x, y) \<in> A. P x y \<Longrightarrow>
  (\<And>x y. (x, y) \<in> A \<Longrightarrow> P x y \<Longrightarrow> Q) \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>(x, y)\<in>A. P x y; \<And>x y. \<lbrakk>(x, y) \<in> A; P x y\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
[PROOF STEP]
by blast


[STATEMENT]
lemma ball_eq_sym: "\<forall>(x, y) \<in> S. f x y = g x y \<Longrightarrow> \<forall>(x, y) \<in> S. g x y = f x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(x, y)\<in>S. f x y = g x y \<Longrightarrow> \<forall>(x, y)\<in>S. g x y = f x y
[PROOF STEP]
by auto


[STATEMENT]
lemma wf_measure_size: "wf (measure size)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (measure size)
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "i < \<parallel>xs\<parallel> \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = xs\<langle>i\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < \<parallel>xs\<parallel> \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = xs\<langle>i\<rangle>
[PROOF STEP]
apply (induct xs arbitrary: i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i < \<parallel>[]\<parallel> \<Longrightarrow> ([] @ ys)\<langle>i\<rangle> = []\<langle>i\<rangle>
 2. \<And>a xs i. \<lbrakk>\<And>i. i < \<parallel>xs\<parallel> \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = xs\<langle>i\<rangle>; i < \<parallel>a \<Colon> xs\<parallel>\<rbrakk> \<Longrightarrow> ((a \<Colon> xs) @ ys)\<langle>i\<rangle> = (a \<Colon> xs)\<langle>i\<rangle>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>\<And>i. i < \<parallel>xs\<parallel> \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = xs\<langle>i\<rangle>; i < \<parallel>a \<Colon> xs\<parallel>\<rbrakk> \<Longrightarrow> ((a \<Colon> xs) @ ys)\<langle>i\<rangle> = (a \<Colon> xs)\<langle>i\<rangle>
[PROOF STEP]
apply (case_tac i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs i. \<lbrakk>\<And>i. i < \<parallel>xs\<parallel> \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = xs\<langle>i\<rangle>; i < \<parallel>a \<Colon> xs\<parallel>; i = 0\<rbrakk> \<Longrightarrow> ((a \<Colon> xs) @ ys)\<langle>i\<rangle> = (a \<Colon> xs)\<langle>i\<rangle>
 2. \<And>a xs i nat. \<lbrakk>\<And>i. i < \<parallel>xs\<parallel> \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = xs\<langle>i\<rangle>; i < \<parallel>a \<Colon> xs\<parallel>; i = Suc nat\<rbrakk> \<Longrightarrow> ((a \<Colon> xs) @ ys)\<langle>i\<rangle> = (a \<Colon> xs)\<langle>i\<rangle>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "\<parallel>xs\<parallel> \<le> i \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>xs\<parallel>\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>xs\<parallel> \<le> i \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>xs\<parallel>\<rangle>
[PROOF STEP]
apply (induct xs arbitrary: i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<parallel>[]\<parallel> \<le> i \<Longrightarrow> ([] @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>[]\<parallel>\<rangle>
 2. \<And>a xs i. \<lbrakk>\<And>i. \<parallel>xs\<parallel> \<le> i \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>xs\<parallel>\<rangle>; \<parallel>a \<Colon> xs\<parallel> \<le> i\<rbrakk> \<Longrightarrow> ((a \<Colon> xs) @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>a \<Colon> xs\<parallel>\<rangle>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xs i. \<lbrakk>\<And>i. \<parallel>xs\<parallel> \<le> i \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>xs\<parallel>\<rangle>; \<parallel>a \<Colon> xs\<parallel> \<le> i\<rbrakk> \<Longrightarrow> ((a \<Colon> xs) @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>a \<Colon> xs\<parallel>\<rangle>
[PROOF STEP]
apply (case_tac i)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xs i. \<lbrakk>\<And>i. \<parallel>xs\<parallel> \<le> i \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>xs\<parallel>\<rangle>; \<parallel>a \<Colon> xs\<parallel> \<le> i; i = 0\<rbrakk> \<Longrightarrow> ((a \<Colon> xs) @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>a \<Colon> xs\<parallel>\<rangle>
 2. \<And>a xs i nat. \<lbrakk>\<And>i. \<parallel>xs\<parallel> \<le> i \<Longrightarrow> (xs @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>xs\<parallel>\<rangle>; \<parallel>a \<Colon> xs\<parallel> \<le> i; i = Suc nat\<rbrakk> \<Longrightarrow> ((a \<Colon> xs) @ ys)\<langle>i\<rangle> = ys\<langle>i - \<parallel>a \<Colon> xs\<parallel>\<rangle>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma assoc_set: "ps\<langle>x\<rangle>\<^sub>? = \<lfloor>y\<rfloor> \<Longrightarrow> (x, y) \<in> set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps\<langle>x\<rangle>\<^sub>? = \<lfloor>y\<rfloor> \<Longrightarrow> (x, y) \<in> set ps
[PROOF STEP]
by (induct ps) (auto split: if_split_asm)


[STATEMENT]
lemma map_assoc_None [simp]:
  "ps\<langle>x\<rangle>\<^sub>? = \<bottom> \<Longrightarrow> map (\<lambda>(x, y). (x, f x y)) ps\<langle>x\<rangle>\<^sub>? = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps\<langle>x\<rangle>\<^sub>? = \<bottom> \<Longrightarrow> map (\<lambda>(x, y). (x, f x y)) ps\<langle>x\<rangle>\<^sub>? = \<bottom>
[PROOF STEP]
by (induct ps) auto


[STATEMENT]
lemma rel_mset_free:
  assumes rel: "rel_mset rel X Y" and xs: "mset xs = X"
  shows "\<exists>ys. mset ys = Y \<and> list_all2 rel xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
from rel[unfolded rel_mset_def]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs ys. mset xs = X \<and> mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
obtain xs' ys'
    where xs': "mset xs' = X" and ys': "mset ys' = Y" and xsys': "list_all2 rel xs' ys'"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs ys. mset xs = X \<and> mset ys = Y \<and> list_all2 rel xs ys

goal (1 subgoal):
 1. (\<And>xs' ys'. \<lbrakk>mset xs' = X; mset ys' = Y; list_all2 rel xs' ys'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset xs' = X
mset ys' = Y
list_all2 rel xs' ys'

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
from xs' xs
[PROOF STATE]
proof (chain)
picking this:
mset xs' = X
mset xs = X
[PROOF STEP]
have "mset xs = mset xs'"
[PROOF STATE]
proof (prove)
using this:
mset xs' = X
mset xs = X

goal (1 subgoal):
 1. mset xs = mset xs'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset xs = mset xs'

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
from mset_eq_permutation[OF this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>p. \<lbrakk>p permutes {..<length xs'}; permute_list p xs' = xs\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain f where perm: "f permutes {..<length xs'}" and xs': "permute_list f xs' = xs"
[PROOF STATE]
proof (prove)
using this:
(\<And>p. \<lbrakk>p permutes {..<length xs'}; permute_list p xs' = xs\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f permutes {..<length xs'}; permute_list f xs' = xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f permutes {..<length xs'}
permute_list f xs' = xs

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f permutes {..<length xs'}
permute_list f xs' = xs
[PROOF STEP]
have [simp]: "length xs' = length xs"
[PROOF STATE]
proof (prove)
using this:
f permutes {..<length xs'}
permute_list f xs' = xs

goal (1 subgoal):
 1. length xs' = length xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs' = length xs

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
from permute_list_nth[OF perm, unfolded xs']
[PROOF STATE]
proof (chain)
picking this:
?i < length xs' \<Longrightarrow> xs ! ?i = xs' ! f ?i
[PROOF STEP]
have *: "\<And>i. i < length xs \<Longrightarrow> xs ! i = xs' ! f i"
[PROOF STATE]
proof (prove)
using this:
?i < length xs' \<Longrightarrow> xs ! ?i = xs' ! f ?i

goal (1 subgoal):
 1. \<And>i. i < length xs \<Longrightarrow> xs ! i = xs' ! f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < length xs \<Longrightarrow> xs ! ?i = xs' ! f ?i

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
note [simp] = list_all2_lengthD[OF xsys',symmetric]
[PROOF STATE]
proof (state)
this:
length ys' = length xs'

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
note [simp] = atLeast0LessThan[symmetric]
[PROOF STATE]
proof (state)
this:
{..<?n} = {0..<?n}

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
note bij =  permutes_bij[OF perm]
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
define ys where "ys \<equiv> map (nth ys' \<circ> f) [0..<length ys']"
[PROOF STATE]
proof (state)
this:
ys \<equiv> map ((!) ys' \<circ> f) [0..<length ys']

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ys \<equiv> map ((!) ys' \<circ> f) [0..<length ys']
[PROOF STEP]
have [simp]: "length ys = length ys'"
[PROOF STATE]
proof (prove)
using this:
ys \<equiv> map ((!) ys' \<circ> f) [0..<length ys']

goal (1 subgoal):
 1. length ys = length ys'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ys = length ys'

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
have "mset ys = mset (map (nth ys') (map f [0..<length ys']))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ys = mset (map ((!) ys') (map f [0..<length ys']))
[PROOF STEP]
unfolding ys_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (map ((!) ys' \<circ> f) [0..<length ys']) = mset (map ((!) ys') (map f [0..<length ys']))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset ys = mset (map ((!) ys') (map f [0..<length ys']))

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mset ys = mset (map ((!) ys') (map f [0..<length ys']))

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
have "... = image_mset (nth ys') (image_mset f (mset [0..<length ys']))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (map ((!) ys') (map f [0..<length ys'])) = image_mset ((!) ys') (image_mset f (mset [0..<length ys']))
[PROOF STEP]
by (simp add: multiset.map_comp)
[PROOF STATE]
proof (state)
this:
mset (map ((!) ys') (map f [0..<length ys'])) = image_mset ((!) ys') (image_mset f (mset [0..<length ys']))

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mset (map ((!) ys') (map f [0..<length ys'])) = image_mset ((!) ys') (image_mset f (mset [0..<length ys']))

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
have "(mset [0..<length ys']) = mset_set {0..<length ys'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset [0..<length ys'] = mset_set {0..<length ys'}
[PROOF STEP]
by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set sorted_list_of_set_range)
[PROOF STATE]
proof (state)
this:
mset [0..<length ys'] = mset_set {0..<length ys'}

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mset [0..<length ys'] = mset_set {0..<length ys'}

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
have "image_mset f (...) = mset_set (f ` {..<length ys'})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset f (mset_set {0..<length ys'}) = mset_set (f ` {..<length ys'})
[PROOF STEP]
using subset_inj_on[OF bij_is_inj[OF bij]]
[PROOF STATE]
proof (prove)
using this:
?A \<subseteq> UNIV \<Longrightarrow> inj_on f ?A

goal (1 subgoal):
 1. image_mset f (mset_set {0..<length ys'}) = mset_set (f ` {..<length ys'})
[PROOF STEP]
by (subst image_mset_mset_set, auto)
[PROOF STATE]
proof (state)
this:
image_mset f (mset_set {0..<length ys'}) = mset_set (f ` {..<length ys'})

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
image_mset f (mset_set {0..<length ys'}) = mset_set (f ` {..<length ys'})

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
have "... = mset [0..<length ys']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_set (f ` {..<length ys'}) = mset [0..<length ys']
[PROOF STEP]
using perm
[PROOF STATE]
proof (prove)
using this:
f permutes {..<length xs'}

goal (1 subgoal):
 1. mset_set (f ` {..<length ys'}) = mset [0..<length ys']
[PROOF STEP]
by (simp add: permutes_image)
[PROOF STATE]
proof (state)
this:
mset_set (f ` {..<length ys'}) = mset [0..<length ys']

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mset_set (f ` {..<length ys'}) = mset [0..<length ys']

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
have "image_mset (nth ys') ... = mset ys'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. image_mset ((!) ys') (mset [0..<length ys']) = mset ys'
[PROOF STEP]
by(fold mset_map, unfold map_nth, auto)
[PROOF STATE]
proof (state)
this:
image_mset ((!) ys') (mset [0..<length ys']) = mset ys'

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mset ys = mset ys'
[PROOF STEP]
have "mset ys = Y"
[PROOF STATE]
proof (prove)
using this:
mset ys = mset ys'

goal (1 subgoal):
 1. mset ys = Y
[PROOF STEP]
using ys'
[PROOF STATE]
proof (prove)
using this:
mset ys = mset ys'
mset ys' = Y

goal (1 subgoal):
 1. mset ys = Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset ys = Y

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mset ys = Y

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
have "list_all2 rel xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 rel xs ys
[PROOF STEP]
proof(rule list_all2_all_nthI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs = length ys
 2. \<And>n. n < length xs \<Longrightarrow> rel (xs ! n) (ys ! n)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs = length ys
 2. \<And>n. n < length xs \<Longrightarrow> rel (xs ! n) (ys ! n)
[PROOF STEP]
assume i: "i < length xs"
[PROOF STATE]
proof (state)
this:
i < length xs

goal (2 subgoals):
 1. length xs = length ys
 2. \<And>n. n < length xs \<Longrightarrow> rel (xs ! n) (ys ! n)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
?i < length xs \<Longrightarrow> xs ! ?i = xs' ! f ?i
i < length xs
[PROOF STEP]
have "xs ! i = xs' ! f i"
[PROOF STATE]
proof (prove)
using this:
?i < length xs \<Longrightarrow> xs ! ?i = xs' ! f ?i
i < length xs

goal (1 subgoal):
 1. xs ! i = xs' ! f i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs ! i = xs' ! f i

goal (2 subgoals):
 1. length xs = length ys
 2. \<And>n. n < length xs \<Longrightarrow> rel (xs ! n) (ys ! n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
xs ! i = xs' ! f i

goal (2 subgoals):
 1. length xs = length ys
 2. \<And>n. n < length xs \<Longrightarrow> rel (xs ! n) (ys ! n)
[PROOF STEP]
from i permutes_in_image[OF perm]
[PROOF STATE]
proof (chain)
picking this:
i < length xs
(f ?x \<in> {..<length xs'}) = (?x \<in> {..<length xs'})
[PROOF STEP]
have "rel (xs' ! f i) (ys' ! f i)"
[PROOF STATE]
proof (prove)
using this:
i < length xs
(f ?x \<in> {..<length xs'}) = (?x \<in> {..<length xs'})

goal (1 subgoal):
 1. rel (xs' ! f i) (ys' ! f i)
[PROOF STEP]
by (intro list_all2_nthD[OF xsys'], auto)
[PROOF STATE]
proof (state)
this:
rel (xs' ! f i) (ys' ! f i)

goal (2 subgoals):
 1. length xs = length ys
 2. \<And>n. n < length xs \<Longrightarrow> rel (xs ! n) (ys ! n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rel (xs ! i) (ys' ! f i)
[PROOF STEP]
show "rel (xs ! i) (ys ! i)"
[PROOF STATE]
proof (prove)
using this:
rel (xs ! i) (ys' ! f i)

goal (1 subgoal):
 1. rel (xs ! i) (ys ! i)
[PROOF STEP]
unfolding ys_def
[PROOF STATE]
proof (prove)
using this:
rel (xs ! i) (ys' ! f i)

goal (1 subgoal):
 1. rel (xs ! i) (map ((!) ys' \<circ> f) [0..<length ys'] ! i)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
rel (xs ! i) (ys' ! f i)
i < length xs

goal (1 subgoal):
 1. rel (xs ! i) (map ((!) ys' \<circ> f) [0..<length ys'] ! i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel (xs ! i) (ys ! i)

goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
list_all2 rel xs ys

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mset ys = Y
list_all2 rel xs ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset ys = Y
list_all2 rel xs ys

goal (1 subgoal):
 1. \<exists>ys. mset ys = Y \<and> list_all2 rel xs ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ys. mset ys = Y \<and> list_all2 rel xs ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_mset_split:
  assumes rel: "rel_mset rel (X1+X2) Y"
  shows "\<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
obtain xs1 where xs1: "mset xs1 = X1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs1. mset xs1 = X1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_mset
[PROOF STATE]
proof (prove)
using this:
\<exists>xs. mset xs = ?X

goal (1 subgoal):
 1. (\<And>xs1. mset xs1 = X1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset xs1 = X1

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
obtain xs2 where xs2: "mset xs2 = X2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs2. mset xs2 = X2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_mset
[PROOF STATE]
proof (prove)
using this:
\<exists>xs. mset xs = ?X

goal (1 subgoal):
 1. (\<And>xs2. mset xs2 = X2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset xs2 = X2

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
from xs1 xs2
[PROOF STATE]
proof (chain)
picking this:
mset xs1 = X1
mset xs2 = X2
[PROOF STEP]
have "mset (xs1 @ xs2) = X1 + X2"
[PROOF STATE]
proof (prove)
using this:
mset xs1 = X1
mset xs2 = X2

goal (1 subgoal):
 1. mset (xs1 @ xs2) = X1 + X2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset (xs1 @ xs2) = X1 + X2

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
from rel_mset_free[OF rel this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys. mset ys = Y \<and> list_all2 rel (xs1 @ xs2) ys
[PROOF STEP]
obtain ys
    where ys: "mset ys = Y" "list_all2 rel (xs1 @ xs2) ys"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys. mset ys = Y \<and> list_all2 rel (xs1 @ xs2) ys

goal (1 subgoal):
 1. (\<And>ys. \<lbrakk>mset ys = Y; list_all2 rel (xs1 @ xs2) ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset ys = Y
list_all2 rel (xs1 @ xs2) ys

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset ys = Y
list_all2 rel (xs1 @ xs2) ys
[PROOF STEP]
obtain ys1 ys2
    where ys12: "ys = ys1 @ ys2"
      and xs1ys1: "list_all2 rel xs1 ys1"
      and xs2ys2: "list_all2 rel xs2 ys2"
[PROOF STATE]
proof (prove)
using this:
mset ys = Y
list_all2 rel (xs1 @ xs2) ys

goal (1 subgoal):
 1. (\<And>ys1 ys2. \<lbrakk>ys = ys1 @ ys2; list_all2 rel xs1 ys1; list_all2 rel xs2 ys2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using list_all2_append1
[PROOF STATE]
proof (prove)
using this:
mset ys = Y
list_all2 rel (xs1 @ xs2) ys
list_all2 ?P (?xs @ ?ys) ?zs = (\<exists>us vs. ?zs = us @ vs \<and> length us = length ?xs \<and> length vs = length ?ys \<and> list_all2 ?P ?xs us \<and> list_all2 ?P ?ys vs)

goal (1 subgoal):
 1. (\<And>ys1 ys2. \<lbrakk>ys = ys1 @ ys2; list_all2 rel xs1 ys1; list_all2 rel xs2 ys2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ys = ys1 @ ys2
list_all2 rel xs1 ys1
list_all2 rel xs2 ys2

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
from ys12 ys
[PROOF STATE]
proof (chain)
picking this:
ys = ys1 @ ys2
mset ys = Y
list_all2 rel (xs1 @ xs2) ys
[PROOF STEP]
have "Y = mset ys1 + mset ys2"
[PROOF STATE]
proof (prove)
using this:
ys = ys1 @ ys2
mset ys = Y
list_all2 rel (xs1 @ xs2) ys

goal (1 subgoal):
 1. Y = mset ys1 + mset ys2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y = mset ys1 + mset ys2

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Y = mset ys1 + mset ys2

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
from xs1 xs1ys1
[PROOF STATE]
proof (chain)
picking this:
mset xs1 = X1
list_all2 rel xs1 ys1
[PROOF STEP]
have "rel_mset rel X1 (mset ys1)"
[PROOF STATE]
proof (prove)
using this:
mset xs1 = X1
list_all2 rel xs1 ys1

goal (1 subgoal):
 1. rel_mset rel X1 (mset ys1)
[PROOF STEP]
unfolding rel_mset_def
[PROOF STATE]
proof (prove)
using this:
mset xs1 = X1
list_all2 rel xs1 ys1

goal (1 subgoal):
 1. \<exists>xs ys. mset xs = X1 \<and> mset ys = mset ys1 \<and> list_all2 rel xs ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rel_mset rel X1 (mset ys1)

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_mset rel X1 (mset ys1)

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
from xs2 xs2ys2
[PROOF STATE]
proof (chain)
picking this:
mset xs2 = X2
list_all2 rel xs2 ys2
[PROOF STEP]
have "rel_mset rel X2 (mset ys2)"
[PROOF STATE]
proof (prove)
using this:
mset xs2 = X2
list_all2 rel xs2 ys2

goal (1 subgoal):
 1. rel_mset rel X2 (mset ys2)
[PROOF STEP]
unfolding rel_mset_def
[PROOF STATE]
proof (prove)
using this:
mset xs2 = X2
list_all2 rel xs2 ys2

goal (1 subgoal):
 1. \<exists>xs ys. mset xs = X2 \<and> mset ys = mset ys2 \<and> list_all2 rel xs ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rel_mset rel X2 (mset ys2)

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Y = mset ys1 + mset ys2
rel_mset rel X1 (mset ys1)
rel_mset rel X2 (mset ys2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Y = mset ys1 + mset ys2
rel_mset rel X1 (mset ys1)
rel_mset rel X2 (mset ys2)

goal (1 subgoal):
 1. \<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2
[PROOF STEP]
by (subst exI[of _ "mset ys1"], subst exI[of _ "mset ys2"],auto)
[PROOF STATE]
proof (state)
this:
\<exists>Y1 Y2. Y = Y1 + Y2 \<and> rel_mset rel X1 Y1 \<and> rel_mset rel X2 Y2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_mset_OO:
  assumes AB: "rel_mset R A B" and BC: "rel_mset S B C"
  shows "rel_mset (R OO S) A C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_mset (R OO S) A C
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_mset (R OO S) A C
[PROOF STEP]
from AB
[PROOF STATE]
proof (chain)
picking this:
rel_mset R A B
[PROOF STEP]
obtain as bs where A_as: "A = mset as" and B_bs: "B = mset bs" and as_bs: "list_all2 R as bs"
[PROOF STATE]
proof (prove)
using this:
rel_mset R A B

goal (1 subgoal):
 1. (\<And>as bs. \<lbrakk>A = mset as; B = mset bs; list_all2 R as bs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: rel_mset_def)
[PROOF STATE]
proof (state)
this:
A = mset as
B = mset bs
list_all2 R as bs

goal (1 subgoal):
 1. rel_mset (R OO S) A C
[PROOF STEP]
from rel_mset_free[OF BC] B_bs
[PROOF STATE]
proof (chain)
picking this:
mset ?xs = B \<Longrightarrow> \<exists>ys. mset ys = C \<and> list_all2 S ?xs ys
B = mset bs
[PROOF STEP]
obtain cs where C_cs: "C = mset cs" and bs_cs: "list_all2 S bs cs"
[PROOF STATE]
proof (prove)
using this:
mset ?xs = B \<Longrightarrow> \<exists>ys. mset ys = C \<and> list_all2 S ?xs ys
B = mset bs

goal (1 subgoal):
 1. (\<And>cs. \<lbrakk>C = mset cs; list_all2 S bs cs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C = mset cs
list_all2 S bs cs

goal (1 subgoal):
 1. rel_mset (R OO S) A C
[PROOF STEP]
from list_all2_trans[OF _ as_bs bs_cs, of "R OO S"] A_as C_cs
[PROOF STATE]
proof (chain)
picking this:
(\<And>a b c. \<lbrakk>R a b; S b c\<rbrakk> \<Longrightarrow> (R OO S) a c) \<Longrightarrow> list_all2 (R OO S) as cs
A = mset as
C = mset cs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>a b c. \<lbrakk>R a b; S b c\<rbrakk> \<Longrightarrow> (R OO S) a c) \<Longrightarrow> list_all2 (R OO S) as cs
A = mset as
C = mset cs

goal (1 subgoal):
 1. rel_mset (R OO S) A C
[PROOF STEP]
by (auto simp: rel_mset_def)
[PROOF STATE]
proof (state)
this:
rel_mset (R OO S) A C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_mset_zip_right:
  assumes "length xs = length ys" "mset ys' = mset ys"
  shows "\<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
mset ys' = mset ys

goal (1 subgoal):
 1. \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys)
[PROOF STEP]
proof (induct xs ys arbitrary: ys' rule: list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ys'. mset ys' = mset [] \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip [] [])
 2. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
mset ys' = mset []

goal (2 subgoals):
 1. \<And>ys'. mset ys' = mset [] \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip [] [])
 2. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
mset ys' = mset []

goal (1 subgoal):
 1. \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip [] [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip [] [])

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
case (Cons x xs y ys ys')
[PROOF STATE]
proof (state)
this:
length xs = length ys
mset ?ys' = mset ys \<Longrightarrow> \<exists>xs'. length ?ys' = length xs' \<and> mset (zip xs' ?ys') = mset (zip xs ys)
mset ys' = mset (y # ys)

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
obtain j where j_len: "j < length ys'" and nth_j: "ys' ! j = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j < length ys'; ys' ! j = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Cons.prems in_set_conv_nth list.set_intros(1) mset_eq_setD)
[PROOF STATE]
proof (state)
this:
j < length ys'
ys' ! j = y

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
define ysa where "ysa = take j ys' @ drop (Suc j) ys'"
[PROOF STATE]
proof (state)
this:
ysa = take j ys' @ drop (Suc j) ys'

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
have "mset ys' = {#y#} + mset ysa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ys' = {#y#} + mset ysa
[PROOF STEP]
unfolding ysa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset ys' = {#y#} + mset (take j ys' @ drop (Suc j) ys')
[PROOF STEP]
using j_len nth_j
[PROOF STATE]
proof (prove)
using this:
j < length ys'
ys' ! j = y

goal (1 subgoal):
 1. mset ys' = {#y#} + mset (take j ys' @ drop (Suc j) ys')
[PROOF STEP]
by (metis Cons_nth_drop_Suc union_mset_add_mset_right add_mset_remove_trivial add_diff_cancel_left'
        append_take_drop_id mset.simps(2) mset_append)
[PROOF STATE]
proof (state)
this:
mset ys' = {#y#} + mset ysa

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
hence ms_y: "mset ysa = mset ys"
[PROOF STATE]
proof (prove)
using this:
mset ys' = {#y#} + mset ysa

goal (1 subgoal):
 1. mset ysa = mset ys
[PROOF STEP]
by (simp add: Cons.prems)
[PROOF STATE]
proof (state)
this:
mset ysa = mset ys

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mset ysa = mset ys
[PROOF STEP]
obtain xsa where
    len_a: "length ysa = length xsa" and ms_a: "mset (zip xsa ysa) = mset (zip xs ys)"
[PROOF STATE]
proof (prove)
using this:
mset ysa = mset ys

goal (1 subgoal):
 1. (\<And>xsaa. \<lbrakk>length ysa = length xsaa; mset (zip xsaa ysa) = mset (zip xs ys)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons.hyps(2)
[PROOF STATE]
proof (prove)
using this:
mset ysa = mset ys
mset ?ys' = mset ys \<Longrightarrow> \<exists>xs'. length ?ys' = length xs' \<and> mset (zip xs' ?ys') = mset (zip xs ys)

goal (1 subgoal):
 1. (\<And>xsaa. \<lbrakk>length ysa = length xsaa; mset (zip xsaa ysa) = mset (zip xs ys)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length ysa = length xsa
mset (zip xsa ysa) = mset (zip xs ys)

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
define xs' where "xs' = take j xsa @ x # drop j xsa"
[PROOF STATE]
proof (state)
this:
xs' = take j xsa @ x # drop j xsa

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
have ys': "ys' = take j ysa @ y # drop j ysa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys' = take j ysa @ y # drop j ysa
[PROOF STEP]
using ms_y j_len nth_j Cons.prems ysa_def
[PROOF STATE]
proof (prove)
using this:
mset ysa = mset ys
j < length ys'
ys' ! j = y
mset ys' = mset (y # ys)
ysa = take j ys' @ drop (Suc j) ys'

goal (1 subgoal):
 1. ys' = take j ysa @ y # drop j ysa
[PROOF STEP]
by (metis append_eq_append_conv append_take_drop_id diff_Suc_Suc Cons_nth_drop_Suc length_Cons
      length_drop size_mset)
[PROOF STATE]
proof (state)
this:
ys' = take j ysa @ y # drop j ysa

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
have j_len': "j \<le> length ysa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<le> length ysa
[PROOF STEP]
using j_len ys' ysa_def
[PROOF STATE]
proof (prove)
using this:
j < length ys'
ys' = take j ysa @ y # drop j ysa
ysa = take j ys' @ drop (Suc j) ys'

goal (1 subgoal):
 1. j \<le> length ysa
[PROOF STEP]
by (metis add_Suc_right append_take_drop_id length_Cons length_append less_eq_Suc_le not_less)
[PROOF STATE]
proof (state)
this:
j \<le> length ysa

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
have "length ys' = length xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ys' = length xs'
[PROOF STEP]
unfolding xs'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ys' = length (take j xsa @ x # drop j xsa)
[PROOF STEP]
using Cons.prems len_a ms_y
[PROOF STATE]
proof (prove)
using this:
mset ys' = mset (y # ys)
length ysa = length xsa
mset ysa = mset ys

goal (1 subgoal):
 1. length ys' = length (take j xsa @ x # drop j xsa)
[PROOF STEP]
by (metis add_Suc_right append_take_drop_id length_Cons length_append mset_eq_length)
[PROOF STATE]
proof (state)
this:
length ys' = length xs'

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length ys' = length xs'

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
have "mset (zip xs' ys') = mset (zip (x # xs) (y # ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
unfolding ys' xs'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (zip (take j xsa @ x # drop j xsa) (take j ysa @ y # drop j ysa)) = mset (zip (x # xs) (y # ys))
[PROOF STEP]
apply (rule HOL.trans[OF mset_zip_take_Cons_drop_twice])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. length xsa = length ysa
 2. j \<le> length xsa
 3. add_mset (x, y) (mset (zip xsa ysa)) = mset (zip (x # xs) (y # ys))
[PROOF STEP]
using j_len'
[PROOF STATE]
proof (prove)
using this:
j \<le> length ysa

goal (3 subgoals):
 1. length xsa = length ysa
 2. j \<le> length xsa
 3. add_mset (x, y) (mset (zip xsa ysa)) = mset (zip (x # xs) (y # ys))
[PROOF STEP]
by (auto simp: len_a ms_a)
[PROOF STATE]
proof (state)
this:
mset (zip xs' ys') = mset (zip (x # xs) (y # ys))

goal (1 subgoal):
 1. \<And>x xs y ys ys'. \<lbrakk>length xs = length ys; \<And>ys'. mset ys' = mset ys \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip xs ys); mset ys' = mset (y # ys)\<rbrakk> \<Longrightarrow> \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length ys' = length xs'
mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length ys' = length xs'
mset (zip xs' ys') = mset (zip (x # xs) (y # ys))

goal (1 subgoal):
 1. \<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs'. length ys' = length xs' \<and> mset (zip xs' ys') = mset (zip (x # xs) (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_all2_reorder_right_invariance:
  assumes rel: "list_all2 R xs ys" and ms_y: "mset ys' = mset ys"
  shows "\<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs
[PROOF STEP]
have len: "length xs = length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
using rel list_all2_conv_all_nth
[PROOF STATE]
proof (prove)
using this:
list_all2 R xs ys
list_all2 ?P ?xs ?ys = (length ?xs = length ?ys \<and> (\<forall>i<length ?xs. ?P (?xs ! i) (?ys ! i)))

goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs = length ys

goal (1 subgoal):
 1. \<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs
[PROOF STEP]
obtain xs' where
    len': "length xs' = length ys'" and ms_xy: "mset (zip xs' ys') = mset (zip xs ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs'. \<lbrakk>length xs' = length ys'; mset (zip xs' ys') = mset (zip xs ys)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using len ms_y
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
mset ys' = mset ys

goal (1 subgoal):
 1. (\<And>xs'. \<lbrakk>length xs' = length ys'; mset (zip xs' ys') = mset (zip xs ys)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis ex_mset_zip_right)
[PROOF STATE]
proof (state)
this:
length xs' = length ys'
mset (zip xs' ys') = mset (zip xs ys)

goal (1 subgoal):
 1. \<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs
[PROOF STEP]
have "list_all2 R xs' ys'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 R xs' ys'
[PROOF STEP]
using assms(1) len' ms_xy
[PROOF STATE]
proof (prove)
using this:
list_all2 R xs ys
length xs' = length ys'
mset (zip xs' ys') = mset (zip xs ys)

goal (1 subgoal):
 1. list_all2 R xs' ys'
[PROOF STEP]
unfolding list_all2_iff
[PROOF STATE]
proof (prove)
using this:
length xs = length ys \<and> (\<forall>(x, y)\<in>set (zip xs ys). R x y)
length xs' = length ys'
mset (zip xs' ys') = mset (zip xs ys)

goal (1 subgoal):
 1. length xs' = length ys' \<and> (\<forall>(x, y)\<in>set (zip xs' ys'). R x y)
[PROOF STEP]
by (blast dest: mset_eq_setD)
[PROOF STATE]
proof (state)
this:
list_all2 R xs' ys'

goal (1 subgoal):
 1. \<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all2 R xs' ys'

goal (1 subgoal):
 1. \<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs
[PROOF STEP]
have "mset xs' = mset xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset xs' = mset xs
[PROOF STEP]
using len len' ms_xy map_fst_zip mset_map
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
length xs' = length ys'
mset (zip xs' ys') = mset (zip xs ys)
length ?xs = length ?ys \<Longrightarrow> map fst (zip ?xs ?ys) = ?xs
mset (map ?f ?xs) = image_mset ?f (mset ?xs)

goal (1 subgoal):
 1. mset xs' = mset xs
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
mset xs' = mset xs

goal (1 subgoal):
 1. \<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
list_all2 R xs' ys'
mset xs' = mset xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
list_all2 R xs' ys'
mset xs' = mset xs

goal (1 subgoal):
 1. \<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xs'. list_all2 R xs' ys' \<and> mset xs' = mset xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_mset_via_perm: "rel_mset rel (mset xs) (mset ys) \<longleftrightarrow> (\<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_mset rel (mset xs) (mset ys) = (\<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys)
[PROOF STEP]
proof (unfold rel_mset_def, intro iffI, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa \<Longrightarrow> \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys
 2. \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys \<Longrightarrow> \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa

goal (2 subgoals):
 1. \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa \<Longrightarrow> \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys
 2. \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys \<Longrightarrow> \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
obtain zs ws where zs: "mset zs = mset xs" and ws: "mset ws = mset ys" and zsws: "list_all2 rel zs ws"
[PROOF STATE]
proof (prove)
using this:
\<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa

goal (1 subgoal):
 1. (\<And>zs ws. \<lbrakk>mset zs = mset xs; mset ws = mset ys; list_all2 rel zs ws\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset zs = mset xs
mset ws = mset ys
list_all2 rel zs ws

goal (2 subgoals):
 1. \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa \<Longrightarrow> \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys
 2. \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys \<Longrightarrow> \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
note list_all2_reorder_right_invariance[OF zsws ws[symmetric], unfolded zs]
[PROOF STATE]
proof (state)
this:
\<exists>xs'. list_all2 rel xs' ys \<and> mset xs' = mset xs

goal (2 subgoals):
 1. \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa \<Longrightarrow> \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys
 2. \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys \<Longrightarrow> \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs'. list_all2 rel xs' ys \<and> mset xs' = mset xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>xs'. list_all2 rel xs' ys \<and> mset xs' = mset xs

goal (1 subgoal):
 1. \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys
[PROOF STEP]
by (auto dest: sym)
[PROOF STATE]
proof (state)
this:
\<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys

goal (1 subgoal):
 1. \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys \<Longrightarrow> \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys \<Longrightarrow> \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys

goal (1 subgoal):
 1. \<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys \<Longrightarrow> \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>zs. mset xs = mset zs \<and> list_all2 rel zs ys

goal (1 subgoal):
 1. \<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>xsa ysa. mset xsa = mset xs \<and> mset ysa = mset ys \<and> list_all2 rel xsa ysa

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sequence_number_increases:
  "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), _, (\<xi>', _)). sn \<xi> \<le> sn \<xi>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). sn \<xi> \<le> sn \<xi>')
[PROOF STEP]
by inv_cterms


[STATEMENT]
lemma sequence_number_one_or_bigger:
  "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, _). 1 \<le> sn \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). 1 \<le> sn \<xi>)
[PROOF STEP]
by (rule onll_step_to_invariantI [OF sequence_number_increases])
     (auto simp: \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V_def)


[STATEMENT]
lemma sequence_number_increases':
  "paodv i \<TTurnstile>\<^sub>A (\<lambda>((\<xi>, _), _, (\<xi>', _)). sn \<xi> \<le> sn \<xi>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). sn \<xi> \<le> sn \<xi>')
[PROOF STEP]
by (rule step_invariant_weakenE [OF sequence_number_increases]) (auto dest!: onllD)


[STATEMENT]
lemma sequence_number_one_or_bigger':
  "paodv i \<TTurnstile> (\<lambda>(\<xi>, _). 1 \<le> sn \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (\<lambda>(\<xi>, uu_). 1 \<le> sn \<xi>)
[PROOF STEP]
by (rule invariant_weakenE [OF sequence_number_one_or_bigger]) auto


[STATEMENT]
lemma sip_in_kD:
  "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> ({PAodv-:7} \<union> {PAodv-:5} \<union> {PRrep-:0..PRrep-:1}
                                     \<union> {PRreq-:0..PRreq-:3}) \<longrightarrow> sip \<xi> \<in> kD (rt \<xi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:7} \<union> {PAodv-:5} \<union> {PRrep-:0..PRrep-:1} \<union> {PRreq-:0..PRreq-:3} \<longrightarrow> sip \<xi> \<in> kD (rt \<xi>))
[PROOF STEP]
by inv_cterms


[STATEMENT]
lemma rrep_1_update_changes:
  "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l = PRrep-:1 \<longrightarrow>
                        rt \<xi> \<noteq> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, hops \<xi> + 1, sip \<xi>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l = PRrep-:1 \<longrightarrow> rt \<xi> \<noteq> update (rt \<xi>) (dip \<xi>) (dsn \<xi>, kno, val, hops \<xi> + 1, sip \<xi>))
[PROOF STEP]
by inv_cterms


[STATEMENT]
lemma includes_nhip:
  "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD(rt \<xi>). the (nhop (rt \<xi>) dip)\<in>kD(rt \<xi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
fix ip and \<xi> \<xi>' :: state
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
assume "\<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>)"
         and "\<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) ip (0, unk, val, Suc 0, ip)\<rparr>"
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>)
\<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) ip (0, unk, val, Suc 0, ip)\<rparr>

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
hence "\<forall>dip\<in>kD (rt \<xi>).
               the (nhop (update (rt \<xi>) ip (0, unk, val, Suc 0, ip)) dip) = ip
             \<or> the (nhop (update (rt \<xi>) ip (0, unk, val, Suc 0, ip)) dip) \<in> kD (rt \<xi>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>)
\<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) ip (0, unk, val, Suc 0, ip)\<rparr>

goal (1 subgoal):
 1. \<forall>dip\<in>kD (rt \<xi>). the (nhop (update (rt \<xi>) ip (0, unk, val, Suc 0, ip)) dip) = ip \<or> the (nhop (update (rt \<xi>) ip (0, unk, val, Suc 0, ip)) dip) \<in> kD (rt \<xi>)
[PROOF STEP]
by clarsimp (metis nhop_update_unk_val update_another)
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD (rt \<xi>). the (nhop (update (rt \<xi>) ip (0, unk, val, Suc 0, ip)) dip) = ip \<or> the (nhop (update (rt \<xi>) ip (0, unk, val, Suc 0, ip)) dip) \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (rt ?\<xi>2) dip) \<in> kD (rt ?\<xi>2); ?\<xi>'2 = ?\<xi>2\<lparr>rt := update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)\<rparr>\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)) dip) = ?ip2 \<or> the (nhop (update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)) dip) \<in> kD (rt ?\<xi>2)

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
note one_hop = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (rt ?\<xi>2) dip) \<in> kD (rt ?\<xi>2); ?\<xi>'2 = ?\<xi>2\<lparr>rt := update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)\<rparr>\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)) dip) = ?ip2 \<or> the (nhop (update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)) dip) \<in> kD (rt ?\<xi>2)

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (rt ?\<xi>2) dip) \<in> kD (rt ?\<xi>2); ?\<xi>'2 = ?\<xi>2\<lparr>rt := update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)\<rparr>\<rbrakk> \<Longrightarrow> \<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)) dip) = ?ip2 \<or> the (nhop (update (rt ?\<xi>2) ?ip2 (0, unk, val, Suc 0, ?ip2)) dip) \<in> kD (rt ?\<xi>2)

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
fix ip sip sn hops and \<xi> \<xi>' :: state
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
assume "\<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>)"
          and "\<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)\<rparr>"
          and "sip \<in> kD (rt \<xi>)"
[PROOF STATE]
proof (state)
this:
\<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>)
\<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)\<rparr>
sip \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
hence "(the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) ip) = ip
               \<or> the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) ip) \<in> kD (rt \<xi>))
               \<and> (\<forall>dip\<in>kD (rt \<xi>).
                    the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) dip) = ip
                    \<or> the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) dip) \<in> kD (rt \<xi>))"
[PROOF STATE]
proof (prove)
using this:
\<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>)
\<xi>' = \<xi>\<lparr>rt := update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)\<rparr>
sip \<in> kD (rt \<xi>)

goal (1 subgoal):
 1. (the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) ip) = ip \<or> the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) ip) \<in> kD (rt \<xi>)) \<and> (\<forall>dip\<in>kD (rt \<xi>). the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) dip) = ip \<or> the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
by (metis kD_update_unchanged nhop_update_changed update_another)
[PROOF STATE]
proof (state)
this:
(the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) ip) = ip \<or> the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) ip) \<in> kD (rt \<xi>)) \<and> (\<forall>dip\<in>kD (rt \<xi>). the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) dip) = ip \<or> the (nhop (update (rt \<xi>) ip (sn, kno, val, Suc hops, sip)) dip) \<in> kD (rt \<xi>))

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (rt ?\<xi>2) dip) \<in> kD (rt ?\<xi>2); ?\<xi>'2 = ?\<xi>2\<lparr>rt := update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)\<rparr>; ?sip2 \<in> kD (rt ?\<xi>2)\<rbrakk> \<Longrightarrow> (the (nhop (update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = ?ip2 \<or> the (nhop (update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) \<in> kD (rt ?\<xi>2)) \<and> (\<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)) dip) = ?ip2 \<or> the (nhop (update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)) dip) \<in> kD (rt ?\<xi>2))

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
note nhip_is_sip = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (rt ?\<xi>2) dip) \<in> kD (rt ?\<xi>2); ?\<xi>'2 = ?\<xi>2\<lparr>rt := update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)\<rparr>; ?sip2 \<in> kD (rt ?\<xi>2)\<rbrakk> \<Longrightarrow> (the (nhop (update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) = ?ip2 \<or> the (nhop (update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)) ?ip2) \<in> kD (rt ?\<xi>2)) \<and> (\<forall>dip\<in>kD (rt ?\<xi>2). the (nhop (update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)) dip) = ?ip2 \<or> the (nhop (update (rt ?\<xi>2) ?ip2 (?sn2, kno, val, Suc ?hops2, ?sip2)) dip) \<in> kD (rt ?\<xi>2))

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf sip_in_kD]
                       solve: one_hop nhip_is_sip)
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). \<forall>dip\<in>kD (rt \<xi>). the (nhop (rt \<xi>) dip) \<in> kD (rt \<xi>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma known_destinations_increase:
  "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), _, (\<xi>', _)). kD (rt \<xi>) \<subseteq> kD (rt \<xi>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). kD (rt \<xi>) \<subseteq> kD (rt \<xi>'))
[PROOF STEP]
by (inv_cterms simp add: subset_insertI)


[STATEMENT]
lemma rreqs_increase:
  "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), _, (\<xi>', _)). rreqs \<xi> \<subseteq> rreqs \<xi>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). rreqs \<xi> \<subseteq> rreqs \<xi>')
[PROOF STEP]
by (inv_cterms simp add: subset_insertI)


[STATEMENT]
lemma dests_bigger_than_sqn:
  "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:15..PAodv-:17}
                                 \<union> {PPkt-:7..PPkt-:9}
                                 \<union> {PRreq-:9..PRreq-:11}
                                 \<union> {PRreq-:17..PRreq-:19}
                                 \<union> {PRrep-:8..PRrep-:10}
                                 \<union> {PRerr-:1..PRerr-:4} \<union> {PRerr-:6}
                         \<longrightarrow> (\<forall>ip\<in>dom(dests \<xi>). ip\<in>kD(rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:15..PAodv-:17} \<union> {PPkt-:7..PPkt-:9} \<union> {PRreq-:9..PRreq-:11} \<union> {PRreq-:17..PRreq-:19} \<union> {PRrep-:8..PRrep-:10} \<union> {PRerr-:1..PRerr-:4} \<union> {PRerr-:6} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:15..PAodv-:17} \<union> {PPkt-:7..PPkt-:9} \<union> {PRreq-:9..PRreq-:11} \<union> {PRreq-:17..PRreq-:19} \<union> {PRrep-:8..PRrep-:10} \<union> {PRerr-:1..PRerr-:4} \<union> {PRerr-:6} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)))
[PROOF STEP]
have sqninv:
      "\<And>dests rt rsn ip.
       \<lbrakk> \<forall>ip\<in>dom(dests). ip\<in>kD(rt) \<and> sqn rt ip \<le> the (dests ip); dests ip = Some rsn \<rbrakk>
        \<Longrightarrow> sqn (invalidate rt dests) ip \<le> rsn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dests rt rsn ip. \<lbrakk>\<forall>ip\<in>dom dests. ip \<in> kD rt \<and> sqn rt ip \<le> the (dests ip); dests ip = Some rsn\<rbrakk> \<Longrightarrow> sqn (invalidate rt dests) ip \<le> rsn
[PROOF STEP]
by (rule sqn_invalidate_in_dests [THEN eq_imp_le], assumption) auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>ip\<in>dom ?dests. ip \<in> kD ?rt \<and> sqn ?rt ip \<le> the (?dests ip); ?dests ?ip = Some ?rsn\<rbrakk> \<Longrightarrow> sqn (invalidate ?rt ?dests) ?ip \<le> ?rsn

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:15..PAodv-:17} \<union> {PPkt-:7..PPkt-:9} \<union> {PRreq-:9..PRreq-:11} \<union> {PRreq-:17..PRreq-:19} \<union> {PRrep-:8..PRrep-:10} \<union> {PRerr-:1..PRerr-:4} \<union> {PRerr-:6} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)))
[PROOF STEP]
have indests:
      "\<And>dests rt rsn ip.
       \<lbrakk> \<forall>ip\<in>dom(dests). ip\<in>kD(rt) \<and> sqn rt ip \<le> the (dests ip); dests ip = Some rsn \<rbrakk>
        \<Longrightarrow> ip\<in>kD(rt) \<and> sqn rt ip \<le> rsn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>dests rt rsn ip. \<lbrakk>\<forall>ip\<in>dom dests. ip \<in> kD rt \<and> sqn rt ip \<le> the (dests ip); dests ip = Some rsn\<rbrakk> \<Longrightarrow> ip \<in> kD rt \<and> sqn rt ip \<le> rsn
[PROOF STEP]
by (metis domI option.sel)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>ip\<in>dom ?dests. ip \<in> kD ?rt \<and> sqn ?rt ip \<le> the (?dests ip); ?dests ?ip = Some ?rsn\<rbrakk> \<Longrightarrow> ?ip \<in> kD ?rt \<and> sqn ?rt ?ip \<le> ?rsn

goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:15..PAodv-:17} \<union> {PPkt-:7..PPkt-:9} \<union> {PRreq-:9..PRreq-:11} \<union> {PRreq-:17..PRreq-:19} \<union> {PRrep-:8..PRrep-:10} \<union> {PRerr-:1..PRerr-:4} \<union> {PRerr-:6} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:15..PAodv-:17} \<union> {PPkt-:7..PPkt-:9} \<union> {PRreq-:9..PRreq-:11} \<union> {PRreq-:17..PRreq-:19} \<union> {PRrep-:8..PRrep-:10} \<union> {PRerr-:1..PRerr-:4} \<union> {PRerr-:6} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)))
[PROOF STEP]
by inv_cterms
         (clarsimp split: if_split_asm option.split_asm
                   elim!: sqninv indests)+
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:15..PAodv-:17} \<union> {PPkt-:7..PPkt-:9} \<union> {PRreq-:9..PRreq-:11} \<union> {PRreq-:17..PRreq-:19} \<union> {PRrep-:8..PRrep-:10} \<union> {PRerr-:1..PRerr-:4} \<union> {PRerr-:6} \<longrightarrow> (\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sqns_increase:
   "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), _, (\<xi>', _)). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
fix \<xi> :: state
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
assume *: "\<forall>ip\<in>dom(dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)"
[PROOF STATE]
proof (state)
this:
\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)

goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
have "\<forall>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip
[PROOF STEP]
fix ip
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)
[PROOF STEP]
have "ip\<notin>dom(dests \<xi>) \<or> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ip\<in>dom (dests \<xi>). ip \<in> kD (rt \<xi>) \<and> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)

goal (1 subgoal):
 1. ip \<notin> dom (dests \<xi>) \<or> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ip \<notin> dom (dests \<xi>) \<or> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)

goal (1 subgoal):
 1. \<And>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip
[PROOF STEP]
thus "sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip"
[PROOF STATE]
proof (prove)
using this:
ip \<notin> dom (dests \<xi>) \<or> sqn (rt \<xi>) ip \<le> the (dests \<xi> ip)

goal (1 subgoal):
 1. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip
[PROOF STEP]
by (metis domI invalidate_sqn option.sel)
[PROOF STATE]
proof (state)
this:
sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>ip. sqn (rt \<xi>) ip \<le> sqn (invalidate (rt \<xi>) (dests \<xi>)) ip

goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>ip\<in>dom (dests ?\<xi>2). ip \<in> kD (rt ?\<xi>2) \<and> sqn (rt ?\<xi>2) ip \<le> the (dests ?\<xi>2 ip) \<Longrightarrow> \<forall>ip. sqn (rt ?\<xi>2) ip \<le> sqn (invalidate (rt ?\<xi>2) (dests ?\<xi>2)) ip

goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
note solve_invalidate = this
[PROOF STATE]
proof (state)
this:
\<forall>ip\<in>dom (dests ?\<xi>2). ip \<in> kD (rt ?\<xi>2) \<and> sqn (rt ?\<xi>2) ip \<le> the (dests ?\<xi>2 ip) \<Longrightarrow> \<forall>ip. sqn (rt ?\<xi>2) ip \<le> sqn (invalidate (rt ?\<xi>2) (dests ?\<xi>2)) ip

goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf dests_bigger_than_sqn]
                    simp add: solve_invalidate)
[PROOF STATE]
proof (state)
this:
paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), uu_, \<xi>', uu_). \<forall>ip. sqn (rt \<xi>) ip \<le> sqn (rt \<xi>') ip)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ip_constant:
  "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, _). ip \<xi> = i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). ip \<xi> = i)
[PROOF STEP]
by (inv_cterms simp add: \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V_def)


[STATEMENT]
lemma sender_ip_valid':
  "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), a, _). anycast (\<lambda>m. not_Pkt m \<longrightarrow> msg_sender m = ip \<xi>) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (\<lambda>m. not_Pkt m \<longrightarrow> msg_sender m = ip \<xi>) a)
[PROOF STEP]
by inv_cterms


[STATEMENT]
lemma sender_ip_valid:
  "paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, _), a, _). anycast (\<lambda>m. not_Pkt m \<longrightarrow> msg_sender m = i) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile>\<^sub>A onll \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>((\<xi>, uu_), a, uu_). anycast (\<lambda>m. not_Pkt m \<longrightarrow> msg_sender m = i) a)
[PROOF STEP]
by (rule step_invariant_weaken_with_invariantE [OF ip_constant sender_ip_valid'])
     (auto dest!: onlD onllD)


[STATEMENT]
lemma received_msg_inv:
  "paodv i \<TTurnstile> (recvmsg P \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:1} \<longrightarrow> P (msg \<xi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg P \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). l \<in> {PAodv-:1} \<longrightarrow> P (msg \<xi>))
[PROOF STEP]
by inv_cterms


[STATEMENT]
lemma sip_not_ip':
  "paodv i \<TTurnstile> (recvmsg (\<lambda>m. not_Pkt m \<longrightarrow> msg_sender m \<noteq> i) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, _). sip \<xi> \<noteq> ip \<xi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. not_Pkt m \<longrightarrow> msg_sender m \<noteq> i) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). sip \<xi> \<noteq> ip \<xi>)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]
                          onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
                simp add: clear_locals_sip_not_ip') clarsimp+


[STATEMENT]
lemma sip_not_ip:
  "paodv i \<TTurnstile> (recvmsg (\<lambda>m. not_Pkt m \<longrightarrow> msg_sender m \<noteq> i) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, _). sip \<xi> \<noteq> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> (recvmsg (\<lambda>m. not_Pkt m \<longrightarrow> msg_sender m \<noteq> i) \<rightarrow>) onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). sip \<xi> \<noteq> i)
[PROOF STEP]
by (inv_cterms inv add: onl_invariant_sterms [OF aodv_wf received_msg_inv]
                          onl_invariant_sterms [OF aodv_wf ip_constant [THEN invariant_restrict_inD]]
                simp add: clear_locals_sip_not_ip') clarsimp+


[STATEMENT]
lemma hop_count_positive:
  "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, _). \<forall>ip\<in>kD (rt \<xi>). the (dhops (rt \<xi>) ip) \<ge> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, uu_). \<forall>ip\<in>kD (rt \<xi>). 1 \<le> the (dhops (rt \<xi>) ip))
[PROOF STEP]
by (inv_cterms) auto


[STATEMENT]
lemma rreq_dip_in_vD_dip_eq_ip:
  "paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PRreq-:14} \<longrightarrow> dip \<xi> \<in> vD(rt \<xi>))
                            \<and> (l \<in> {PRreq-:5, PRreq-:6} \<longrightarrow> dip \<xi> = ip \<xi>)
                            \<and> (l \<in> {PRreq-:13..PRreq-:14} \<longrightarrow> dip \<xi> \<noteq> ip \<xi>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paodv i \<TTurnstile> onl \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (\<lambda>(\<xi>, l). (l \<in> {PRreq-:14} \<longrightarrow> dip \<xi> \<in> vD (rt \<xi>)) \<and> (l \<in> {PRreq-:5, PRreq-:6} \<longrightarrow> dip \<xi> = ip \<xi>) \<and> (l \<in> {PRreq-:13..PRreq-:14} \<longrightarrow> dip \<xi> \<noteq> ip \<xi>))
[PROOF STEP]
by inv_cterms