[STATEMENT]
lemma evaluate_match_total: "\<exists>s' r. evaluate_match True env s v pes v' (s', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v pes v' (s', r)
[PROOF STEP]
proof (induction pes arbitrary: env s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>env s. \<exists>s' r. evaluate_match True env s v [] v' (s', r)
 2. \<And>a pes env s. (\<And>env s. \<exists>s' r. evaluate_match True env s v pes v' (s', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (a # pes) v' (s', r)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>env s. \<exists>s' r. evaluate_match True env s v [] v' (s', r)
 2. \<And>a pes env s. (\<And>env s. \<exists>s' r. evaluate_match True env s v pes v' (s', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (a # pes) v' (s', r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v [] v' (s', r)
[PROOF STEP]
by (metis mat_empty)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True env s v [] v' (s', r)

goal (1 subgoal):
 1. \<And>a pes env s. (\<And>env s. \<exists>s' r. evaluate_match True env s v pes v' (s', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (a # pes) v' (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a pes env s. (\<And>env s. \<exists>s' r. evaluate_match True env s v pes v' (s', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (a # pes) v' (s', r)
[PROOF STEP]
case (Cons pe pes)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True ?env ?s v pes v' (s', r)

goal (1 subgoal):
 1. \<And>a pes env s. (\<And>env s. \<exists>s' r. evaluate_match True env s v pes v' (s', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (a # pes) v' (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate_match True ?env ?s v pes v' (s', r)
[PROOF STEP]
obtain p e where "pe = (p, e)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate_match True ?env ?s v pes v' (s', r)

goal (1 subgoal):
 1. (\<And>p e. pe = (p, e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
pe = (p, e)

goal (1 subgoal):
 1. \<And>a pes env s. (\<And>env s. \<exists>s' r. evaluate_match True env s v pes v' (s', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (a # pes) v' (s', r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
proof (cases "allDistinct (pat_bindings p [])")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
case distinct: True
[PROOF STATE]
proof (state)
this:
allDistinct (pat_bindings p [])

goal (2 subgoals):
 1. allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
proof (cases "pmatch (c env) (refs s) p v []")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pmatch (c env) (refs s) p v [] = No_match \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. pmatch (c env) (refs s) p v [] = Match_type_error \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 3. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
case No_match
[PROOF STATE]
proof (state)
this:
pmatch (c env) (refs s) p v [] = No_match

goal (3 subgoals):
 1. pmatch (c env) (refs s) p v [] = No_match \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. pmatch (c env) (refs s) p v [] = Match_type_error \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 3. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
have "\<exists>s' r. evaluate_match True env s v pes v' (s', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v pes v' (s', r)
[PROOF STEP]
by (rule Cons)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True env s v pes v' (s', r)

goal (3 subgoals):
 1. pmatch (c env) (refs s) p v [] = No_match \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. pmatch (c env) (refs s) p v [] = Match_type_error \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 3. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate_match True env s v pes v' (s', r)
[PROOF STEP]
obtain s' r where "evaluate_match True env s v pes v' (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate_match True env s v pes v' (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate_match True env s v pes v' (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate_match True env s v pes v' (s', r)

goal (3 subgoals):
 1. pmatch (c env) (refs s) p v [] = No_match \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. pmatch (c env) (refs s) p v [] = Match_type_error \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 3. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
unfolding \<open>pe = _\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v ((p, e) # pes) v' (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_match True env s v ((p, e) # pes) v' (?s', ?r1)
[PROOF STEP]
apply (rule mat_cons2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s) p v [] = No_match \<and> evaluate_match True env s v pes v' (?s', ?r1)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. allDistinct (pat_bindings p [])
 2. pmatch (c env) (refs s) p v [] = No_match
 3. evaluate_match True env s v pes v' (?s', ?r1)
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)

goal (2 subgoals):
 1. pmatch (c env) (refs s) p v [] = Match_type_error \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pmatch (c env) (refs s) p v [] = Match_type_error \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
case Match_type_error
[PROOF STATE]
proof (state)
this:
pmatch (c env) (refs s) p v [] = Match_type_error

goal (2 subgoals):
 1. pmatch (c env) (refs s) p v [] = Match_type_error \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
 2. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pmatch (c env) (refs s) p v [] = Match_type_error
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pmatch (c env) (refs s) p v [] = Match_type_error

goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
unfolding \<open>pe = _\<close>
[PROOF STATE]
proof (prove)
using this:
pmatch (c env) (refs s) p v [] = Match_type_error

goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v ((p, e) # pes) v' (s', r)
[PROOF STEP]
by (metis mat_cons3)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)

goal (1 subgoal):
 1. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
case (Match env')
[PROOF STATE]
proof (state)
this:
pmatch (c env) (refs s) p v [] = Match env'

goal (1 subgoal):
 1. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
have "\<exists>s' r. evaluate True (env \<lparr> sem_env.v := (nsAppend (alist_to_ns env') (sem_env.v env)) \<rparr>) s e (s', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate True (update_v (\<lambda>_. nsAppend (alist_to_ns env') (sem_env.v env)) env) s e (s', r)
[PROOF STEP]
by (metis evaluate_total)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate True (update_v (\<lambda>_. nsAppend (alist_to_ns env') (sem_env.v env)) env) s e (s', r)

goal (1 subgoal):
 1. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s' r. evaluate True (update_v (\<lambda>_. nsAppend (alist_to_ns env') (sem_env.v env)) env) s e (s', r)
[PROOF STEP]
obtain s' r where "evaluate True (env \<lparr> sem_env.v := (nsAppend (alist_to_ns env') (sem_env.v env)) \<rparr>) s e (s', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s' r. evaluate True (update_v (\<lambda>_. nsAppend (alist_to_ns env') (sem_env.v env)) env) s e (s', r)

goal (1 subgoal):
 1. (\<And>s' r. evaluate True (update_v (\<lambda>_. nsAppend (alist_to_ns env') (sem_env.v env)) env) s e (s', r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
evaluate True (update_v (\<lambda>_. nsAppend (alist_to_ns env') (sem_env.v env)) env) s e (s', r)

goal (1 subgoal):
 1. \<And>x3. pmatch (c env) (refs s) p v [] = Match x3 \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
unfolding \<open>pe = _\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v ((p, e) # pes) v' (s', r)
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evaluate_match True env s v ((p, e) # pes) v' (?s', ?r1)
[PROOF STEP]
apply (rule mat_cons1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. allDistinct (pat_bindings p []) \<and> pmatch (c env) (refs s) p v [] = Match ?env'2 \<and> evaluate True (update_v (\<lambda>_. nsAppend (alist_to_ns ?env'2) (sem_env.v env)) env) s e (?s', ?r1)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. allDistinct (pat_bindings p [])
 2. pmatch (c env) (refs s) p v [] = Match ?env'2
 3. evaluate True (update_v (\<lambda>_. nsAppend (alist_to_ns ?env'2) (sem_env.v env)) env) s e (?s', ?r1)
[PROOF STEP]
apply fact+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)

goal (1 subgoal):
 1. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> allDistinct (pat_bindings p [])

goal (1 subgoal):
 1. \<not> allDistinct (pat_bindings p []) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> allDistinct (pat_bindings p [])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> allDistinct (pat_bindings p [])

goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)
[PROOF STEP]
unfolding \<open>pe = _\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> allDistinct (pat_bindings p [])

goal (1 subgoal):
 1. \<exists>s' r. evaluate_match True env s v ((p, e) # pes) v' (s', r)
[PROOF STEP]
by (metis mat_cons4)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_match True env s v (pe # pes) v' (s', r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [code, code del]:
  "(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_of_class.term_of = term_of_class.term_of
[PROOF STEP]
..


[STATEMENT]
lemma Heap_cases [case_names succeed fail]:
  fixes f and h
  assumes succeed: "\<And>x h'. execute f h = Some (x, h') \<Longrightarrow> P"
  assumes fail: "execute f h = None \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute f h = Some (?x, ?h') \<Longrightarrow> P
execute f h = None \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (cases "execute f h") auto


[STATEMENT]
lemma Heap_execute [simp]:
  "Heap (execute f) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Heap (execute f) = f
[PROOF STEP]
by (cases f) simp_all


[STATEMENT]
lemma Heap_eqI:
  "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. execute f h = execute g h) \<Longrightarrow> f = g
[PROOF STEP]
by (cases f, cases g) (auto simp: fun_eq_iff)


[STATEMENT]
lemma execute_Let [execute_simps]:
  "execute (let x = t in f x) = (let x = t in execute (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (Let t f) = (let x = t in execute (f x))
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma execute_tap [execute_simps]:
  "execute (tap f) h = Some (f h, h, 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (tap f) h = Some (f h, h, 1)
[PROOF STEP]
by (simp add: tap_def)


[STATEMENT]
lemma execute_heap [execute_simps]:
  "execute (heap f) = Some \<circ> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (heap f) = Some \<circ> f
[PROOF STEP]
by (simp add: heap_def)


[STATEMENT]
lemma execute_guard [execute_simps]:
  "\<not> P h \<Longrightarrow> execute (guard P f) h = None"
  "P h \<Longrightarrow> execute (guard P f) h = Some (f h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> P h \<Longrightarrow> execute (guard P f) h = None) &&& (P h \<Longrightarrow> execute (guard P f) h = Some (f h))
[PROOF STEP]
by (simp_all add: guard_def)


[STATEMENT]
lemma successI:
  "execute f h \<noteq> None \<Longrightarrow> success f h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute f h \<noteq> None \<Longrightarrow> success f h
[PROOF STEP]
by (simp add: success_def)


[STATEMENT]
lemma successE:
  assumes "success f h"
  obtains r h' where "execute f h = Some (r, h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r h'. execute f h = Some (r, h') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
success f h

goal (1 subgoal):
 1. (\<And>r h'. execute f h = Some (r, h') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: success_def)


[STATEMENT]
lemma success_tapI [success_intros]:
  "success (tap f) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (tap f) h
[PROOF STEP]
by (rule successI) (simp add: execute_simps)


[STATEMENT]
lemma success_heapI [success_intros]:
  "success (heap f) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (heap f) h
[PROOF STEP]
by (rule successI) (simp add: execute_simps)


[STATEMENT]
lemma success_guardI [success_intros]:
  "P h \<Longrightarrow> success (guard P f) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P h \<Longrightarrow> success (guard P f) h
[PROOF STEP]
by (rule successI) (simp add: execute_guard)


[STATEMENT]
lemma success_LetI [success_intros]:
  "x = t \<Longrightarrow> success (f x) h \<Longrightarrow> success (let x = t in f x) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = t; success (f x) h\<rbrakk> \<Longrightarrow> success (Let t f) h
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma success_ifI:
  "(c \<Longrightarrow> success t h) \<Longrightarrow> (\<not> c \<Longrightarrow> success e h) \<Longrightarrow>
    success (if c then t else e) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<Longrightarrow> success t h; \<not> c \<Longrightarrow> success e h\<rbrakk> \<Longrightarrow> success (if c then t else e) h
[PROOF STEP]
by (simp add: success_def)


[STATEMENT]
lemma effectI:
  "execute c h = Some (r, h',n) \<Longrightarrow> effect c h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute c h = Some (r, h', n) \<Longrightarrow> effect c h h' r n
[PROOF STEP]
by (simp add: effect_def)


[STATEMENT]
lemma effectE:
  assumes "effect c h h' r n"
  obtains "r = fst (the (execute c h))"
    and "h' = fst (snd (the (execute c h)))"
    and "n = snd (snd (the (execute c h)))"
    and "success c h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (rule that)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> r = fst (the (execute c h))
 2. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> h' = fst (snd (the (execute c h)))
 3. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> n = snd (snd (the (execute c h)))
 4. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> success c h
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
effect c h h' r n
[PROOF STEP]
have *: "execute c h = Some (r, h',n)"
[PROOF STATE]
proof (prove)
using this:
effect c h h' r n

goal (1 subgoal):
 1. execute c h = Some (r, h', n)
[PROOF STEP]
by (simp add: effect_def)
[PROOF STATE]
proof (state)
this:
execute c h = Some (r, h', n)

goal (4 subgoals):
 1. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> r = fst (the (execute c h))
 2. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> h' = fst (snd (the (execute c h)))
 3. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> n = snd (snd (the (execute c h)))
 4. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> success c h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
execute c h = Some (r, h', n)
[PROOF STEP]
show "success c h"
[PROOF STATE]
proof (prove)
using this:
execute c h = Some (r, h', n)

goal (1 subgoal):
 1. success c h
[PROOF STEP]
by (simp add: success_def)
[PROOF STATE]
proof (state)
this:
success c h

goal (3 subgoals):
 1. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> r = fst (the (execute c h))
 2. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> h' = fst (snd (the (execute c h)))
 3. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> n = snd (snd (the (execute c h)))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
execute c h = Some (r, h', n)
[PROOF STEP]
have "fst (the (execute c h)) = r" and "fst (snd (the (execute c h))) = h'"
       and "snd (snd (the (execute c h))) = n"
[PROOF STATE]
proof (prove)
using this:
execute c h = Some (r, h', n)

goal (1 subgoal):
 1. fst (the (execute c h)) = r &&& fst (snd (the (execute c h))) = h' &&& snd (snd (the (execute c h))) = n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
fst (the (execute c h)) = r
fst (snd (the (execute c h))) = h'
snd (snd (the (execute c h))) = n

goal (3 subgoals):
 1. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> r = fst (the (execute c h))
 2. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> h' = fst (snd (the (execute c h)))
 3. (\<lbrakk>r = fst (the (execute c h)); h' = fst (snd (the (execute c h))); n = snd (snd (the (execute c h))); success c h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> n = snd (snd (the (execute c h)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (the (execute c h)) = r
fst (snd (the (execute c h))) = h'
snd (snd (the (execute c h))) = n
[PROOF STEP]
show "r = fst (the (execute c h))"
    and "h' = fst (snd (the (execute c h)))"
    and "n = snd (snd (the (execute c h)))"
[PROOF STATE]
proof (prove)
using this:
fst (the (execute c h)) = r
fst (snd (the (execute c h))) = h'
snd (snd (the (execute c h))) = n

goal (1 subgoal):
 1. r = fst (the (execute c h)) &&& h' = fst (snd (the (execute c h))) &&& n = snd (snd (the (execute c h)))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
r = fst (the (execute c h))
h' = fst (snd (the (execute c h)))
n = snd (snd (the (execute c h)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma effect_success:
  "effect c h h' r n \<Longrightarrow> success c h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect c h h' r n \<Longrightarrow> success c h
[PROOF STEP]
by (simp add: effect_def success_def)


[STATEMENT]
lemma success_effectE:
  assumes "success c h"
  obtains r h' n where "effect c h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h' r n. effect c h h' r n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
success c h

goal (1 subgoal):
 1. (\<And>h' r n. effect c h h' r n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: effect_def success_def)


[STATEMENT]
lemma effect_deterministic:
  assumes "effect f h h' a n"
    and "effect f h h'' b n'"
  shows "a = b" and "h' = h''" and "n = n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b &&& h' = h'' &&& n = n'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect f h h' a n
effect f h h'' b n'

goal (1 subgoal):
 1. a = b &&& h' = h'' &&& n = n'
[PROOF STEP]
unfolding effect_def
[PROOF STATE]
proof (prove)
using this:
execute f h = Some (a, h', n)
execute f h = Some (b, h'', n')

goal (1 subgoal):
 1. a = b &&& h' = h'' &&& n = n'
[PROOF STEP]
by auto


[STATEMENT]
lemma effect_LetI [effect_intros]:
  assumes "x = t" "effect (f x) h h' r n"
  shows "effect (let x = t in f x) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (Let t f) h h' r n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x = t
effect (f x) h h' r n

goal (1 subgoal):
 1. effect (Let t f) h h' r n
[PROOF STEP]
by simp


[STATEMENT]
lemma effect_LetE [effect_elims]:
  assumes "effect (let x = t in f x) h h' r n"
  obtains "effect (f t) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (effect (f t) h h' r n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (Let t f) h h' r n

goal (1 subgoal):
 1. (effect (f t) h h' r n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp


[STATEMENT]
lemma effect_ifI:
  assumes "c \<Longrightarrow> effect t h h' r n"
    and "\<not> c \<Longrightarrow> effect e h h' r n"
  shows "effect (if c then t else e) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (if c then t else e) h h' r n
[PROOF STEP]
by (cases c) (simp_all add: assms)


[STATEMENT]
lemma effect_ifE:
  assumes "effect (if c then t else e) h h' r n"
  obtains "c" "effect t h h' r n"
    | "\<not> c" "effect e h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>c; effect t h h' r n\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> c; effect e h h' r n\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (if c then t else e) h h' r n

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>c; effect t h h' r n\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>\<not> c; effect e h h' r n\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases c) simp_all


[STATEMENT]
lemma effect_tapI [effect_intros]:
  assumes "h' = h" "r = f h"
  shows "effect (tap f) h h' r 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (tap f) h h' r 1
[PROOF STEP]
by (rule effectI) (simp add: assms execute_simps)


[STATEMENT]
lemma effect_tapE [effect_elims]:
  assumes "effect (tap f) h h' r n"
  obtains "h' = h" and "r = f h" and "n=1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>h' = h; r = f h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (tap f) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>h' = h; r = f h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (auto simp add: execute_simps)


[STATEMENT]
lemma effect_heapI [effect_intros]:
  assumes  "n = snd (snd (f h))" "h' = fst (snd (f h))" "r = fst (f h)"
  shows "effect (heap f) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (heap f) h h' r n
[PROOF STEP]
by (rule effectI) (simp add: assms execute_simps)


[STATEMENT]
lemma effect_heapE [effect_elims]:
  assumes "effect (heap f) h h' r n"
  obtains "h' = fst (snd (f h))" and "n = snd (snd (f h))" and "r = fst (f h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>h' = fst (snd (f h)); n = snd (snd (f h)); r = fst (f h)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (heap f) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>h' = fst (snd (f h)); n = snd (snd (f h)); r = fst (f h)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (simp add: execute_simps)


[STATEMENT]
lemma effect_guardI [effect_intros]:
  assumes "P h" "h' = fst (snd (f h))" "n = snd (snd (f h))" "r = fst (f h)"
  shows "effect (guard P f) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (guard P f) h h' r n
[PROOF STEP]
by (rule effectI) (simp add: assms execute_simps)


[STATEMENT]
lemma effect_guardE [effect_elims]:
  assumes "effect (guard P f) h h' r n"
  obtains "h' = fst (snd (f h))" "n = snd (snd (f h))" "r = fst (f h)" "P h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>h' = fst (snd (f h)); n = snd (snd (f h)); r = fst (f h); P h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (guard P f) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>h' = fst (snd (f h)); n = snd (snd (f h)); r = fst (f h); P h\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE)
    (auto simp add: execute_simps elim!: successE, cases "P h", auto simp add: execute_simps)


[STATEMENT]
lemma execute_return [execute_simps]:
  "execute (return x) = Some \<circ> (\<lambda>h. (x,h,1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (return x) = Some \<circ> (\<lambda>h. (x, h, 1))
[PROOF STEP]
by (simp add: return_def execute_simps)


[STATEMENT]
lemma success_returnI [success_intros]:
  "success (return x) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (return x) h
[PROOF STEP]
by (rule successI) (simp add: execute_simps)


[STATEMENT]
lemma effect_returnI [effect_intros]:
  "h = h' \<Longrightarrow> effect (return x) h h' x 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = h' \<Longrightarrow> effect (return x) h h' x 1
[PROOF STEP]
by (rule effectI) (simp add: execute_simps)


[STATEMENT]
lemma effect_returnE [effect_elims]:
  assumes "effect (return x) h h' r n"
  obtains "r = x" "h' = h" "n=1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = x; h' = h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (return x) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>r = x; h' = h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (simp add: execute_simps)


[STATEMENT]
lemma execute_ureturn [execute_simps]:
  "execute (ureturn x) = Some \<circ> (\<lambda>h. (x,h,0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (ureturn x) = Some \<circ> (\<lambda>h. (x, h, 0))
[PROOF STEP]
by (simp add: ureturn_def execute_simps)


[STATEMENT]
lemma success_ureturnI [success_intros]:
  "success (ureturn x) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (ureturn x) h
[PROOF STEP]
by (rule successI) (simp add: execute_simps)


[STATEMENT]
lemma effect_ureturnI [effect_intros]:
  "h = h' \<Longrightarrow> effect (ureturn x) h h' x 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = h' \<Longrightarrow> effect (ureturn x) h h' x 0
[PROOF STEP]
by (rule effectI) (simp add: execute_simps)


[STATEMENT]
lemma effect_ureturnE [effect_elims]:
  assumes "effect (ureturn x) h h' r n"
  obtains "r = x" "h' = h" "n=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = x; h' = h; n = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (ureturn x) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>r = x; h' = h; n = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (simp add: execute_simps)


[STATEMENT]
lemma execute_raise [execute_simps]:
  "execute (raise s) = (\<lambda>_. None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (raise s) = Map.empty
[PROOF STEP]
by (simp add: raise_def)


[STATEMENT]
lemma effect_raiseE [effect_elims]:
  assumes "effect (raise x) h h' r n"
  obtains "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (False \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (raise x) h h' r n

goal (1 subgoal):
 1. (False \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (simp add: success_def execute_simps)


[STATEMENT]
lemma timeFrame_zero[simp]: "timeFrame 0 h = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. timeFrame 0 h = h
[PROOF STEP]
apply(cases h)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. h = None \<Longrightarrow> timeFrame 0 h = h
 2. \<And>a. h = Some a \<Longrightarrow> timeFrame 0 h = h
[PROOF STEP]
by auto


[STATEMENT]
lemma timeFrame_assoc[simp]: "timeFrame n (timeFrame n' f) = timeFrame (n+n') f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. timeFrame n (timeFrame n' f) = timeFrame (n + n') f
[PROOF STEP]
by (metis (no_types, lifting) ab_semigroup_add_class.add_ac(1) timeFrame.elims timeFrame.simps(1))


[STATEMENT]
lemma execute_bind [execute_simps]:
  "execute f h = Some (x, h',n) \<Longrightarrow> execute (f \<bind> g) h = timeFrame n (execute (g x) h')"
  "execute f h = None \<Longrightarrow> execute (f \<bind> g) h = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (execute f h = Some (x, h', n) \<Longrightarrow> execute (f \<bind> g) h = timeFrame n (execute (g x) h')) &&& (execute f h = None \<Longrightarrow> execute (f \<bind> g) h = None)
[PROOF STEP]
by (simp_all add: bind_def)


[STATEMENT]
lemma execute_bind_case:
  "execute (f \<bind> g) h = (case (execute f h) of
    Some (x, h',n) \<Rightarrow> timeFrame n (execute (g x) h') | None \<Rightarrow> None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (f \<bind> g) h = (case execute f h of None \<Rightarrow> None | Some (x, h', n) \<Rightarrow> timeFrame n (execute (g x) h'))
[PROOF STEP]
by (simp add: bind_def)


[STATEMENT]
lemma execute_bind_success:
  "success f h \<Longrightarrow> execute (f \<bind> g) h
         = timeFrame (snd (snd (the (execute f h)))) (execute (g (fst (the (execute f h)))) (fst (snd (the (execute f h)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success f h \<Longrightarrow> execute (f \<bind> g) h = timeFrame (snd (snd (the (execute f h)))) (execute (g (fst (the (execute f h)))) (fst (snd (the (execute f h)))))
[PROOF STEP]
by (cases f h rule: Heap_cases) (auto elim: successE simp add: bind_def)


[STATEMENT]
lemma success_bind_executeI:
  "execute f h = Some (x, h',n) \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<bind> g) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>execute f h = Some (x, h', n); success (g x) h'\<rbrakk> \<Longrightarrow> success (f \<bind> g) h
[PROOF STEP]
by (auto intro!: successI elim: successE simp add: bind_def)


[STATEMENT]
lemma success_bind_effectI [success_intros]:
  "effect f h h' x n \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<bind> g) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>effect f h h' x n; success (g x) h'\<rbrakk> \<Longrightarrow> success (f \<bind> g) h
[PROOF STEP]
by (auto simp add: effect_def success_def bind_def)


[STATEMENT]
lemma effect_bindI [effect_intros]:
  assumes "effect f h h' r n" "effect (g r) h' h'' r' n'"
  shows "effect (f \<bind> g) h h'' r' (n+n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (f \<bind> g) h h'' r' (n + n')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect f h h' r n
effect (g r) h' h'' r' n'

goal (1 subgoal):
 1. effect (f \<bind> g) h h'' r' (n + n')
[PROOF STEP]
apply (auto intro!: effectI elim!: effectE successE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>execute f h = Some (r, h', n); execute (g r) h' = Some (r', h'', n')\<rbrakk> \<Longrightarrow> execute (f \<bind> g) h = Some (r', h'', n + n')
[PROOF STEP]
apply (subst execute_bind, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>execute f h = Some (r, h', n); execute (g r) h' = Some (r', h'', n')\<rbrakk> \<Longrightarrow> timeFrame n (execute (g r) h') = Some (r', h'', n + n')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma effect_bindE [effect_elims]:
  assumes "effect (f \<bind> g) h h'' r' n"
  obtains h' r n1 n2 where "effect f h h' r n1" "effect (g r) h' h'' r' n2" "n = n1 + n2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h' r n1 n2. \<lbrakk>effect f h h' r n1; effect (g r) h' h'' r' n2; n = n1 + n2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (f \<bind> g) h h'' r' n

goal (1 subgoal):
 1. (\<And>h' r n1 n2. \<lbrakk>effect f h h' r n1; effect (g r) h' h'' r' n2; n = n1 + n2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp add: effect_def bind_def split: option.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>h' n2. \<lbrakk>aa = h'; execute (g a) h' = Some (r', h'', n2); n = b + n2\<rbrakk> \<Longrightarrow> thesis; execute f h = Some (a, aa, b); timeFrame b (execute (g a) aa) = Some (r', h'', n)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
(* To cleanup *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>h' n2. \<lbrakk>aa = h'; execute (g a) h' = Some (r', h'', n2); n = b + n2\<rbrakk> \<Longrightarrow> thesis; execute f h = Some (a, aa, b); timeFrame b (execute (g a) aa) = Some (r', h'', n)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (smt Pair_inject option.distinct(1) option.inject timeFrame.elims)


[STATEMENT]
lemma execute_bind_eq_SomeI:
  assumes "execute f h = Some (x, h',n)"
    and "execute (g x) h' = Some (y, h'',n')"
  shows "execute (f \<bind> g) h = Some (y, h'',n+n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (f \<bind> g) h = Some (y, h'', n + n')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute f h = Some (x, h', n)
execute (g x) h' = Some (y, h'', n')

goal (1 subgoal):
 1. execute (f \<bind> g) h = Some (y, h'', n + n')
[PROOF STEP]
by (simp add: bind_def)


[STATEMENT]
lemma [simp]: "wait n \<bind> (%_. wait m) = wait (n+m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wait n \<bind> (\<lambda>_. wait m) = wait (n + m)
[PROOF STEP]
unfolding wait_def bind_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Heap (\<lambda>h. case execute (Heap (\<lambda>h. Some ((), h, n))) h of None \<Rightarrow> None | Some (r, h', n) \<Rightarrow> timeFrame n (execute (Heap (\<lambda>h. Some ((), h, m))) h')) = Heap (\<lambda>h. Some ((), h, n + m))
[PROOF STEP]
by auto


[STATEMENT]
lemma ureturn_bind [execute_simps]: "ureturn x \<bind> f = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ureturn x \<bind> f = f x
[PROOF STEP]
apply (rule Heap_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. execute (ureturn x \<bind> f) h = execute (f x) h
[PROOF STEP]
by (simp add: execute_simps)


[STATEMENT]
lemma return_bind [execute_simps]: "return x \<bind> f = (wait 1) \<then> f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return x \<bind> f = wait 1 \<bind> (\<lambda>_. f x)
[PROOF STEP]
apply (rule Heap_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h. execute (return x \<bind> f) h = execute (wait 1 \<bind> (\<lambda>_. f x)) h
[PROOF STEP]
by (simp add: execute_simps)


[STATEMENT]
lemma bind_return [execute_simps]: "f \<bind> return = wait 1 \<then> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bind> return = wait 1 \<bind> (\<lambda>_. f)
[PROOF STEP]
by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)


[STATEMENT]
lemma bind_ureturn [execute_simps]: "f \<bind> ureturn = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bind> ureturn = f
[PROOF STEP]
by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)


[STATEMENT]
lemma bind_bind [simp]: "(f \<bind> g) \<bind> k = (f :: 'a Heap) \<bind> (\<lambda>x. g x \<bind> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bind> g \<bind> k = f \<bind> (\<lambda>x. g x \<bind> k)
[PROOF STEP]
by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)


[STATEMENT]
lemma raise_bind [simp]: "raise e \<bind> f = raise e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. raise e \<bind> f = raise e
[PROOF STEP]
by (rule Heap_eqI) (simp add: execute_simps)


[STATEMENT]
lemma execute_assert [execute_simps]:
  "P x \<Longrightarrow> execute (assert P x) h  = Some (x, h, 1)"
  "\<not> P x \<Longrightarrow> execute (assert P x) h = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P x \<Longrightarrow> execute (assert P x) h = Some (x, h, 1)) &&& (\<not> P x \<Longrightarrow> execute (assert P x) h = None)
[PROOF STEP]
by (simp_all add: assert_def execute_simps)


[STATEMENT]
lemma success_assertI [success_intros]:
  "P x \<Longrightarrow> success (assert P x) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x \<Longrightarrow> success (assert P x) h
[PROOF STEP]
by (rule successI) (simp add: execute_assert)


[STATEMENT]
lemma effect_assertI [effect_intros]:
  "P x \<Longrightarrow> h' = h \<Longrightarrow> r = x \<Longrightarrow> n = 1 \<Longrightarrow> effect (assert P x) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P x; h' = h; r = x; n = 1\<rbrakk> \<Longrightarrow> effect (assert P x) h h' r n
[PROOF STEP]
by (rule effectI) (simp add: execute_assert)


[STATEMENT]
lemma effect_assertE [effect_elims]:
  assumes "effect (assert P x) h h' r n"
  obtains "P x" "r = x" "h' = h" "n=1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P x; r = x; h' = h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (assert P x) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>P x; r = x; h' = h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (cases "P x", simp_all add: execute_assert success_def)


[STATEMENT]
lemma assert_cong [fundef_cong]:
  assumes "P = P'"
  assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
  shows "(assert P x \<bind> f) = (assert P' x \<bind> f')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. assert P x \<bind> f = assert P' x \<bind> f'
[PROOF STEP]
by (rule Heap_eqI) (insert assms, simp add: assert_def execute_simps)


[STATEMENT]
lemma lift_collapse [simp]:
  "lift f x = return (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift f x = return (f x)
[PROOF STEP]
by (simp add: lift_def)


[STATEMENT]
lemma bind_lift:
  "(f \<bind> lift g) = (f \<bind> (\<lambda>x. return (g x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bind> lift g = f \<bind> (\<lambda>x. return (g x))
[PROOF STEP]
by (simp add: lift_def comp_def)


[STATEMENT]
lemma Heap_lub_empty: "Heap_lub {} = Heap Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Heap_lub {} = Heap Map.empty
[PROOF STEP]
by(simp add: Heap_lub_def img_lub_def fun_lub_def flat_lub_def)


[STATEMENT]
lemma heap_interpretation: "partial_function_definitions Heap_ord Heap_lub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_function_definitions Heap_ord Heap_lub
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partial_function_definitions Heap_ord Heap_lub
[PROOF STEP]
have "partial_function_definitions (fun_ord option_ord) (fun_lub (flat_lub None))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partial_function_definitions option.le_fun option.lub_fun
[PROOF STEP]
by (rule partial_function_lift) (rule flat_interpretation)
[PROOF STATE]
proof (state)
this:
partial_function_definitions option.le_fun option.lub_fun

goal (1 subgoal):
 1. partial_function_definitions Heap_ord Heap_lub
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partial_function_definitions option.le_fun option.lub_fun
[PROOF STEP]
have "partial_function_definitions (img_ord execute (fun_ord option_ord))
      (img_lub execute Heap (fun_lub (flat_lub None)))"
[PROOF STATE]
proof (prove)
using this:
partial_function_definitions option.le_fun option.lub_fun

goal (1 subgoal):
 1. partial_function_definitions (img_ord execute option.le_fun) (img_lub execute Heap option.lub_fun)
[PROOF STEP]
by (rule partial_function_image) (auto intro: Heap_eqI)
[PROOF STATE]
proof (state)
this:
partial_function_definitions (img_ord execute option.le_fun) (img_lub execute Heap option.lub_fun)

goal (1 subgoal):
 1. partial_function_definitions Heap_ord Heap_lub
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partial_function_definitions (img_ord execute option.le_fun) (img_lub execute Heap option.lub_fun)
[PROOF STEP]
show "partial_function_definitions Heap_ord Heap_lub"
[PROOF STATE]
proof (prove)
using this:
partial_function_definitions (img_ord execute option.le_fun) (img_lub execute Heap option.lub_fun)

goal (1 subgoal):
 1. partial_function_definitions Heap_ord Heap_lub
[PROOF STEP]
by (simp only: Heap_ord_def Heap_lub_def)
[PROOF STATE]
proof (state)
this:
partial_function_definitions Heap_ord Heap_lub

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma heap_step_admissible:
  "option.admissible
      (\<lambda>f:: 'a => ('b * 'c* 'd) option. \<forall>h h' r n. f h = Some (r, h',n) \<longrightarrow> P x h h' r n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option.admissible (\<lambda>f. \<forall>h h' r n. f h = Some (r, h', n) \<longrightarrow> P x h h' r n)
[PROOF STEP]
proof (rule ccpo.admissibleI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>Complete_Partial_Order.chain option.le_fun A; A \<noteq> {}; \<forall>xa\<in>A. \<forall>h h' r n. xa h = Some (r, h', n) \<longrightarrow> P x h h' r n\<rbrakk> \<Longrightarrow> \<forall>h h' r n. option.lub_fun A h = Some (r, h', n) \<longrightarrow> P x h h' r n
[PROOF STEP]
fix A :: "('a \<Rightarrow> ('b * 'c * 'd) option) set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>Complete_Partial_Order.chain option.le_fun A; A \<noteq> {}; \<forall>xa\<in>A. \<forall>h h' r n. xa h = Some (r, h', n) \<longrightarrow> P x h h' r n\<rbrakk> \<Longrightarrow> \<forall>h h' r n. option.lub_fun A h = Some (r, h', n) \<longrightarrow> P x h h' r n
[PROOF STEP]
assume ch: "Complete_Partial_Order.chain option.le_fun A"
    and IH: "\<forall>f\<in>A. \<forall>h h' r n. f h = Some (r, h', n) \<longrightarrow> P x h h' r n"
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain option.le_fun A
\<forall>f\<in>A. \<forall>h h' r n. f h = Some (r, h', n) \<longrightarrow> P x h h' r n

goal (1 subgoal):
 1. \<And>A. \<lbrakk>Complete_Partial_Order.chain option.le_fun A; A \<noteq> {}; \<forall>xa\<in>A. \<forall>h h' r n. xa h = Some (r, h', n) \<longrightarrow> P x h h' r n\<rbrakk> \<Longrightarrow> \<forall>h h' r n. option.lub_fun A h = Some (r, h', n) \<longrightarrow> P x h h' r n
[PROOF STEP]
from ch
[PROOF STATE]
proof (chain)
picking this:
Complete_Partial_Order.chain option.le_fun A
[PROOF STEP]
have ch': "\<And>x. Complete_Partial_Order.chain option_ord {y. \<exists>f\<in>A. y = f x}"
[PROOF STATE]
proof (prove)
using this:
Complete_Partial_Order.chain option.le_fun A

goal (1 subgoal):
 1. \<And>x. Complete_Partial_Order.chain option_ord {y. \<exists>f\<in>A. y = f x}
[PROOF STEP]
by (rule chain_fun)
[PROOF STATE]
proof (state)
this:
Complete_Partial_Order.chain option_ord {y. \<exists>f\<in>A. y = f ?x}

goal (1 subgoal):
 1. \<And>A. \<lbrakk>Complete_Partial_Order.chain option.le_fun A; A \<noteq> {}; \<forall>xa\<in>A. \<forall>h h' r n. xa h = Some (r, h', n) \<longrightarrow> P x h h' r n\<rbrakk> \<Longrightarrow> \<forall>h h' r n. option.lub_fun A h = Some (r, h', n) \<longrightarrow> P x h h' r n
[PROOF STEP]
show "\<forall>h h' r n. option.lub_fun A h = Some (r, h', n) \<longrightarrow> P x h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h h' r n. option.lub_fun A h = Some (r, h', n) \<longrightarrow> P x h h' r n
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h h' r n. option.lub_fun A h = Some (r, h', n) \<Longrightarrow> P x h h' r n
[PROOF STEP]
fix h h' r n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h h' r n. option.lub_fun A h = Some (r, h', n) \<Longrightarrow> P x h h' r n
[PROOF STEP]
assume "option.lub_fun A h = Some (r, h', n)"
[PROOF STATE]
proof (state)
this:
option.lub_fun A h = Some (r, h', n)

goal (1 subgoal):
 1. \<And>h h' r n. option.lub_fun A h = Some (r, h', n) \<Longrightarrow> P x h h' r n
[PROOF STEP]
from flat_lub_in_chain[OF ch' this[unfolded fun_lub_def]]
[PROOF STATE]
proof (chain)
picking this:
Some (r, h', n) = None \<or> Some (r, h', n) \<in> {y. \<exists>f\<in>A. y = f h}
[PROOF STEP]
have "Some (r, h', n) \<in> {y. \<exists>f\<in>A. y = f h}"
[PROOF STATE]
proof (prove)
using this:
Some (r, h', n) = None \<or> Some (r, h', n) \<in> {y. \<exists>f\<in>A. y = f h}

goal (1 subgoal):
 1. Some (r, h', n) \<in> {y. \<exists>f\<in>A. y = f h}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Some (r, h', n) \<in> {y. \<exists>f\<in>A. y = f h}

goal (1 subgoal):
 1. \<And>h h' r n. option.lub_fun A h = Some (r, h', n) \<Longrightarrow> P x h h' r n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some (r, h', n) \<in> {y. \<exists>f\<in>A. y = f h}
[PROOF STEP]
have "\<exists>f\<in>A. f h = Some (r, h', n)"
[PROOF STATE]
proof (prove)
using this:
Some (r, h', n) \<in> {y. \<exists>f\<in>A. y = f h}

goal (1 subgoal):
 1. \<exists>f\<in>A. f h = Some (r, h', n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>f\<in>A. f h = Some (r, h', n)

goal (1 subgoal):
 1. \<And>h h' r n. option.lub_fun A h = Some (r, h', n) \<Longrightarrow> P x h h' r n
[PROOF STEP]
with IH
[PROOF STATE]
proof (chain)
picking this:
\<forall>f\<in>A. \<forall>h h' r n. f h = Some (r, h', n) \<longrightarrow> P x h h' r n
\<exists>f\<in>A. f h = Some (r, h', n)
[PROOF STEP]
show "P x h h' r n"
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>A. \<forall>h h' r n. f h = Some (r, h', n) \<longrightarrow> P x h h' r n
\<exists>f\<in>A. f h = Some (r, h', n)

goal (1 subgoal):
 1. P x h h' r n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P x h h' r n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>h h' r n. option.lub_fun A h = Some (r, h', n) \<longrightarrow> P x h h' r n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma admissible_heap:
  "heap.admissible (\<lambda>f. \<forall>x h h' r n. effect (f x) h h' r n \<longrightarrow> P x h h' r n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap.admissible (\<lambda>f. \<forall>x h h' r n. effect (f x) h h' r n \<longrightarrow> P x h h' r n)
[PROOF STEP]
proof (rule admissible_fun[OF heap_interpretation])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ccpo.admissible Heap_lub Heap_ord (\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ccpo.admissible Heap_lub Heap_ord (\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n)
[PROOF STEP]
show "ccpo.admissible Heap_lub Heap_ord (\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccpo.admissible Heap_lub Heap_ord (\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n)
[PROOF STEP]
unfolding Heap_ord_def Heap_lub_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccpo.admissible (img_lub execute Heap option.lub_fun) (img_ord execute option.le_fun) (\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n)
[PROOF STEP]
proof (intro admissible_image partial_function_lift flat_interpretation)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. option.admissible ((\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n) \<circ> Heap)
 2. \<And>x y. execute x = execute y \<Longrightarrow> x = y
 3. \<And>x. execute (Heap x) = x
[PROOF STEP]
show "option.admissible ((\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n) \<circ> Heap)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option.admissible ((\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n) \<circ> Heap)
[PROOF STEP]
unfolding comp_def effect_def execute.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. option.admissible (\<lambda>xa. \<forall>h h' r n. xa h = Some (r, h', n) \<longrightarrow> P x h h' r n)
[PROOF STEP]
by (rule heap_step_admissible)
[PROOF STATE]
proof (state)
this:
option.admissible ((\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n) \<circ> Heap)

goal (2 subgoals):
 1. \<And>x y. execute x = execute y \<Longrightarrow> x = y
 2. \<And>x. execute (Heap x) = x
[PROOF STEP]
qed (auto simp add: Heap_eqI)
[PROOF STATE]
proof (state)
this:
ccpo.admissible Heap_lub Heap_ord (\<lambda>a. \<forall>h h' r n. effect a h h' r n \<longrightarrow> P x h h' r n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fixp_induct_heap:
  fixes F :: "'c \<Rightarrow> 'c" and
    U :: "'c \<Rightarrow> 'b \<Rightarrow> 'a Heap" and
    C :: "('b \<Rightarrow> 'a Heap) \<Rightarrow> 'c" and
    P :: "'b \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> bool"
  assumes mono: "\<And>x. monotone (fun_ord Heap_ord) Heap_ord (\<lambda>f. U (F (C f)) x)"
  assumes eq: "f \<equiv> C (ccpo.fixp (fun_lub Heap_lub) (fun_ord Heap_ord) (\<lambda>f. U (F (C f))))"
  assumes inverse2: "\<And>f. U (C f) = f"
  assumes step: "\<And>f x h h' r n. (\<And>x h h' r n. effect (U f x) h h' r n \<Longrightarrow> P x h h' r n)
    \<Longrightarrow> effect (U (F f) x) h h' r n \<Longrightarrow> P x h h' r n"
  assumes defined: "effect (U f x) h h' r n"
  shows "P x h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x h h' r n
[PROOF STEP]
using step defined heap.fixp_induct_uc[of U F C, OF mono eq inverse2 admissible_heap, of P]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x h h' r n. effect (U ?f x) h h' r n \<Longrightarrow> P x h h' r n; effect (U (F ?f) ?x) ?h ?h' ?r ?n\<rbrakk> \<Longrightarrow> P ?x ?h ?h' ?r ?n
effect (U f x) h h' r n
\<lbrakk>\<forall>x h h' r n. effect (Heap Map.empty) h h' r n \<longrightarrow> P x h h' r n; \<And>f. \<forall>x h h' r n. effect (U f x) h h' r n \<longrightarrow> P x h h' r n \<Longrightarrow> \<forall>x h h' r n. effect (U (F f) x) h h' r n \<longrightarrow> P x h h' r n\<rbrakk> \<Longrightarrow> \<forall>x h h' r n. effect (U f x) h h' r n \<longrightarrow> P x h h' r n

goal (1 subgoal):
 1. P x h h' r n
[PROOF STEP]
unfolding effect_def execute.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x h h' r n. execute (U ?f x) h = Some (r, h', n) \<Longrightarrow> P x h h' r n; execute (U (F ?f) ?x) ?h = Some (?r, ?h', ?n)\<rbrakk> \<Longrightarrow> P ?x ?h ?h' ?r ?n
execute (U f x) h = Some (r, h', n)
\<lbrakk>\<forall>x h h' r n. None = Some (r, h', n) \<longrightarrow> P x h h' r n; \<And>f. \<forall>x h h' r n. execute (U f x) h = Some (r, h', n) \<longrightarrow> P x h h' r n \<Longrightarrow> \<forall>x h h' r n. execute (U (F f) x) h = Some (r, h', n) \<longrightarrow> P x h h' r n\<rbrakk> \<Longrightarrow> \<forall>x h h' r n. execute (U f x) h = Some (r, h', n) \<longrightarrow> P x h h' r n

goal (1 subgoal):
 1. P x h h' r n
[PROOF STEP]
by blast


[STATEMENT]
lemma Heap_ordI:
  assumes "\<And>h. execute x h = None \<or> execute x h = execute y h"
  shows "Heap_ord x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Heap_ord x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
execute x ?h = None \<or> execute x ?h = execute y ?h

goal (1 subgoal):
 1. Heap_ord x y
[PROOF STEP]
unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
[PROOF STATE]
proof (prove)
using this:
execute x ?h = None \<or> execute x ?h = execute y ?h

goal (1 subgoal):
 1. \<forall>xa. execute x xa = None \<or> execute x xa = execute y xa
[PROOF STEP]
by blast


[STATEMENT]
lemma Heap_ordE:
  assumes "Heap_ord x y"
  obtains "execute x h = None" | "execute x h = execute y h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>execute x h = None \<Longrightarrow> thesis; execute x h = execute y h \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Heap_ord x y

goal (1 subgoal):
 1. \<lbrakk>execute x h = None \<Longrightarrow> thesis; execute x h = execute y h \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding Heap_ord_def img_ord_def fun_ord_def flat_ord_def
[PROOF STATE]
proof (prove)
using this:
\<forall>xa. execute x xa = None \<or> execute x xa = execute y xa

goal (1 subgoal):
 1. \<lbrakk>execute x h = None \<Longrightarrow> thesis; execute x h = execute y h \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim blast


[STATEMENT]
lemma bind_mono [partial_function_mono]:
  assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
  shows "mono_Heap (\<lambda>f. B f \<bind> (\<lambda>y. C y f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone heap.le_fun Heap_ord (\<lambda>f. B f \<bind> (\<lambda>y. C y f))
[PROOF STEP]
proof (rule monotoneI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (B x \<bind> (\<lambda>y. C y x)) (B y \<bind> (\<lambda>ya. C ya y))
[PROOF STEP]
fix f g :: "'a \<Rightarrow> 'b Heap"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (B x \<bind> (\<lambda>y. C y x)) (B y \<bind> (\<lambda>ya. C ya y))
[PROOF STEP]
assume fg: "fun_ord Heap_ord f g"
[PROOF STATE]
proof (state)
this:
heap.le_fun f g

goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (B x \<bind> (\<lambda>y. C y x)) (B y \<bind> (\<lambda>ya. C ya y))
[PROOF STEP]
from mf
[PROOF STATE]
proof (chain)
picking this:
monotone heap.le_fun Heap_ord B
[PROOF STEP]
have 1: "Heap_ord (B f) (B g)"
[PROOF STATE]
proof (prove)
using this:
monotone heap.le_fun Heap_ord B

goal (1 subgoal):
 1. Heap_ord (B f) (B g)
[PROOF STEP]
by (rule monotoneD) (rule fg)
[PROOF STATE]
proof (state)
this:
Heap_ord (B f) (B g)

goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (B x \<bind> (\<lambda>y. C y x)) (B y \<bind> (\<lambda>ya. C ya y))
[PROOF STEP]
from mg
[PROOF STATE]
proof (chain)
picking this:
monotone heap.le_fun Heap_ord (C ?y)
[PROOF STEP]
have 2: "\<And>y'. Heap_ord (C y' f) (C y' g)"
[PROOF STATE]
proof (prove)
using this:
monotone heap.le_fun Heap_ord (C ?y)

goal (1 subgoal):
 1. \<And>y'. Heap_ord (C y' f) (C y' g)
[PROOF STEP]
by (rule monotoneD) (rule fg)
[PROOF STATE]
proof (state)
this:
Heap_ord (C ?y' f) (C ?y' g)

goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (B x \<bind> (\<lambda>y. C y x)) (B y \<bind> (\<lambda>ya. C ya y))
[PROOF STEP]
have "Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y. C y f))"
    (is "Heap_ord ?L ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y. C y f))
[PROOF STEP]
proof (rule Heap_ordI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h. execute (B f \<bind> (\<lambda>y. C y f)) h = None \<or> execute (B f \<bind> (\<lambda>y. C y f)) h = execute (B g \<bind> (\<lambda>y. C y f)) h
[PROOF STEP]
fix h
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h. execute (B f \<bind> (\<lambda>y. C y f)) h = None \<or> execute (B f \<bind> (\<lambda>y. C y f)) h = execute (B g \<bind> (\<lambda>y. C y f)) h
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
Heap_ord (B f) (B g)
[PROOF STEP]
show "execute ?L h = None \<or> execute ?L h = execute ?R h"
[PROOF STATE]
proof (prove)
using this:
Heap_ord (B f) (B g)

goal (1 subgoal):
 1. execute (B f \<bind> (\<lambda>y. C y f)) h = None \<or> execute (B f \<bind> (\<lambda>y. C y f)) h = execute (B g \<bind> (\<lambda>y. C y f)) h
[PROOF STEP]
by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case)
[PROOF STATE]
proof (state)
this:
execute (B f \<bind> (\<lambda>y. C y f)) h = None \<or> execute (B f \<bind> (\<lambda>y. C y f)) h = execute (B g \<bind> (\<lambda>y. C y f)) h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y. C y f))

goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (B x \<bind> (\<lambda>y. C y x)) (B y \<bind> (\<lambda>ya. C ya y))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y. C y f))

goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (B x \<bind> (\<lambda>y. C y x)) (B y \<bind> (\<lambda>ya. C ya y))
[PROOF STEP]
have "Heap_ord (B g \<bind> (\<lambda>y'. C y' f)) (B g \<bind> (\<lambda>y'. C y' g))"
    (is "Heap_ord ?L ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Heap_ord (B g \<bind> (\<lambda>y'. C y' f)) (B g \<bind> (\<lambda>y'. C y' g))
[PROOF STEP]
proof (rule Heap_ordI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h. execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
fix h
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>h. execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
show "execute ?L h = None \<or> execute ?L h = execute ?R h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
proof (cases "execute (B g) h")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. execute (B g) h = None \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
 2. \<And>a. execute (B g) h = Some a \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
execute (B g) h = None

goal (2 subgoals):
 1. execute (B g) h = None \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
 2. \<And>a. execute (B g) h = Some a \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
execute (B g) h = None
[PROOF STEP]
have "execute ?L h = None"
[PROOF STATE]
proof (prove)
using this:
execute (B g) h = None

goal (1 subgoal):
 1. execute (B g \<bind> (\<lambda>y'. C y' f)) h = None
[PROOF STEP]
by (auto simp: execute_bind_case)
[PROOF STATE]
proof (state)
this:
execute (B g \<bind> (\<lambda>y'. C y' f)) h = None

goal (2 subgoals):
 1. execute (B g) h = None \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
 2. \<And>a. execute (B g) h = Some a \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
execute (B g \<bind> (\<lambda>y'. C y' f)) h = None

goal (1 subgoal):
 1. execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h

goal (1 subgoal):
 1. \<And>a. execute (B g) h = Some a \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. execute (B g) h = Some a \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
case Some
[PROOF STATE]
proof (state)
this:
execute (B g) h = Some a_

goal (1 subgoal):
 1. \<And>a. execute (B g) h = Some a \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
execute (B g) h = Some a_
[PROOF STEP]
obtain r h' n where "execute (B g) h = Some (r, h', n)"
[PROOF STATE]
proof (prove)
using this:
execute (B g) h = Some a_

goal (1 subgoal):
 1. (\<And>r h' n. execute (B g) h = Some (r, h', n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surjective_pairing)
[PROOF STATE]
proof (state)
this:
execute (B g) h = Some (r, h', n)

goal (1 subgoal):
 1. \<And>a. execute (B g) h = Some a \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
execute (B g) h = Some (r, h', n)
[PROOF STEP]
have "execute ?L h = timeFrame n (execute (C r f) h')"
        "execute ?R h = timeFrame n (execute (C r g) h')"
[PROOF STATE]
proof (prove)
using this:
execute (B g) h = Some (r, h', n)

goal (1 subgoal):
 1. execute (B g \<bind> (\<lambda>y'. C y' f)) h = timeFrame n (execute (C r f) h') &&& execute (B g \<bind> (\<lambda>y'. C y' g)) h = timeFrame n (execute (C r g) h')
[PROOF STEP]
by (auto simp: execute_bind_case)
[PROOF STATE]
proof (state)
this:
execute (B g \<bind> (\<lambda>y'. C y' f)) h = timeFrame n (execute (C r f) h')
execute (B g \<bind> (\<lambda>y'. C y' g)) h = timeFrame n (execute (C r g) h')

goal (1 subgoal):
 1. \<And>a. execute (B g) h = Some a \<Longrightarrow> execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
with 2[of r]
[PROOF STATE]
proof (chain)
picking this:
Heap_ord (C r f) (C r g)
execute (B g \<bind> (\<lambda>y'. C y' f)) h = timeFrame n (execute (C r f) h')
execute (B g \<bind> (\<lambda>y'. C y' g)) h = timeFrame n (execute (C r g) h')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Heap_ord (C r f) (C r g)
execute (B g \<bind> (\<lambda>y'. C y' f)) h = timeFrame n (execute (C r f) h')
execute (B g \<bind> (\<lambda>y'. C y' g)) h = timeFrame n (execute (C r g) h')

goal (1 subgoal):
 1. execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h
[PROOF STEP]
apply (auto elim: Heap_ordE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Heap_ord (C r f) (C r g); execute (B g \<bind> (\<lambda>y'. C y' f)) h = timeFrame n (execute (C r f) h'); execute (B g \<bind> (\<lambda>y'. C y' g)) h = timeFrame n (execute (C r g) h'); timeFrame n (execute (C r f) h') \<noteq> timeFrame n (execute (C r g) h')\<rbrakk> \<Longrightarrow> timeFrame n (execute (C r f) h') = None
[PROOF STEP]
by (metis Heap_ordE timeFrame.simps(2))
[PROOF STATE]
proof (state)
this:
execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
execute (B g \<bind> (\<lambda>y'. C y' f)) h = None \<or> execute (B g \<bind> (\<lambda>y'. C y' f)) h = execute (B g \<bind> (\<lambda>y'. C y' g)) h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Heap_ord (B g \<bind> (\<lambda>y'. C y' f)) (B g \<bind> (\<lambda>y'. C y' g))

goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (B x \<bind> (\<lambda>y. C y x)) (B y \<bind> (\<lambda>ya. C ya y))
[PROOF STEP]
finally (heap.leq_trans)
[PROOF STATE]
proof (chain)
picking this:
Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y'. C y' g))
[PROOF STEP]
show "Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y'. C y' g))"
[PROOF STATE]
proof (prove)
using this:
Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y'. C y' g))

goal (1 subgoal):
 1. Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y'. C y' g))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y'. C y' g))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_if_return: "(if b then return c else return d) = return (if b then c else d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if b then return c else return d) = return (if b then c else d)
[PROOF STEP]
by simp


[STATEMENT]
lemma distrib_if_bind: "do { x \<leftarrow> if b then (c::_ Heap) else d; f x } = (if b then do {x \<leftarrow> c; f x} else do { x\<leftarrow>d; f x })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if b then c else d) \<bind> f = (if b then c \<bind> f else d \<bind> f)
[PROOF STEP]
by simp


[STATEMENT]
lemma eqButUIDl_eq[simp,intro!]: "eqButUIDl uid uidl uidl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid uidl uidl
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUIDl_sym:
assumes "eqButUIDl uid uidl uidl1"
shows "eqButUIDl uid uidl1 uidl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid uidl1 uidl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDl uid uidl uidl1

goal (1 subgoal):
 1. eqButUIDl uid uidl1 uidl
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUIDl_trans:
assumes "eqButUIDl uid uidl uidl1" and "eqButUIDl uid uidl1 uidl2"
shows "eqButUIDl uid uidl uidl2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid uidl uidl2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDl uid uidl uidl1
eqButUIDl uid uidl1 uidl2

goal (1 subgoal):
 1. eqButUIDl uid uidl uidl2
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUIDl_remove1_cong:
assumes "eqButUIDl uid uidl uidl1"
shows "eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
have "remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)
[PROOF STEP]
by (simp add: remove1_commute)
[PROOF STATE]
proof (state)
this:
remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
have "\<dots> = remove1 uid' (remove1 uid uidl1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remove1 uid' (remove1 uid uidl) = remove1 uid' (remove1 uid uidl1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDl uid uidl uidl1

goal (1 subgoal):
 1. remove1 uid' (remove1 uid uidl) = remove1 uid' (remove1 uid uidl1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
remove1 uid' (remove1 uid uidl) = remove1 uid' (remove1 uid uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
remove1 uid' (remove1 uid uidl) = remove1 uid' (remove1 uid uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
have "\<dots> = remove1 uid (remove1 uid' uidl1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remove1 uid' (remove1 uid uidl1) = remove1 uid (remove1 uid' uidl1)
[PROOF STEP]
by (simp add: remove1_commute)
[PROOF STATE]
proof (state)
this:
remove1 uid' (remove1 uid uidl1) = remove1 uid (remove1 uid' uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
remove1 uid (remove1 uid' uidl) = remove1 uid (remove1 uid' uidl1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
remove1 uid (remove1 uid' uidl) = remove1 uid (remove1 uid' uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUIDl_snoc_cong:
assumes "eqButUIDl uid uidl uidl1"
and "uid' \<in>\<in> uidl \<longleftrightarrow> uid' \<in>\<in> uidl1"
shows "eqButUIDl uid (uidl ## uid') (uidl1 ## uid')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid (uidl ## uid') (uidl1 ## uid')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDl uid uidl uidl1
(uid' \<in>\<in> uidl) = (uid' \<in>\<in> uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (uidl ## uid') (uidl1 ## uid')
[PROOF STEP]
by (auto simp add: remove1_append remove1_idem)


[STATEMENT]
lemma eqButUIDf_eeq[simp,intro!]: "eqButUIDf frds frds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf frds frds
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds UID1) \<and> eqButUIDl UID1 (frds UID2) (frds UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds uid)
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUIDf_sym:
assumes "eqButUIDf frds frds1" shows "eqButUIDf frds1 frds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf frds1 frds
[PROOF STEP]
using assms eqButUIDl_sym
[PROOF STATE]
proof (prove)
using this:
eqButUIDf frds frds1
eqButUIDl ?uid ?uidl ?uidl1.0 \<Longrightarrow> eqButUIDl ?uid ?uidl1.0 ?uidl

goal (1 subgoal):
 1. eqButUIDf frds1 frds
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)
eqButUIDl ?uid ?uidl ?uidl1.0 \<Longrightarrow> eqButUIDl ?uid ?uidl1.0 ?uidl

goal (1 subgoal):
 1. eqButUIDl UID2 (frds1 UID1) (frds UID1) \<and> eqButUIDl UID1 (frds1 UID2) (frds UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds1 uid = frds uid)
[PROOF STEP]
by presburger


[STATEMENT]
lemma eqButUIDf_trans:
assumes "eqButUIDf frds frds1" and "eqButUIDf frds1 frds2"
shows "eqButUIDf frds frds2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf frds frds2
[PROOF STEP]
using assms eqButUIDl_trans
[PROOF STATE]
proof (prove)
using this:
eqButUIDf frds frds1
eqButUIDf frds1 frds2
\<lbrakk>eqButUIDl ?uid ?uidl ?uidl1.0; eqButUIDl ?uid ?uidl1.0 ?uidl2.0\<rbrakk> \<Longrightarrow> eqButUIDl ?uid ?uidl ?uidl2.0

goal (1 subgoal):
 1. eqButUIDf frds frds2
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)
eqButUIDl UID2 (frds1 UID1) (frds2 UID1) \<and> eqButUIDl UID1 (frds1 UID2) (frds2 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds1 uid = frds2 uid)
\<lbrakk>eqButUIDl ?uid ?uidl ?uidl1.0; eqButUIDl ?uid ?uidl1.0 ?uidl2.0\<rbrakk> \<Longrightarrow> eqButUIDl ?uid ?uidl ?uidl2.0

goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds2 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds2 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds2 uid)
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUIDf_cong:
assumes "eqButUIDf frds frds1"
and "uid = UID1 \<Longrightarrow> eqButUIDl UID2 uu uu1"
and "uid = UID2 \<Longrightarrow> eqButUIDl UID1 uu uu1"
and "uid \<noteq> UID1 \<Longrightarrow> uid \<noteq> UID2 \<Longrightarrow> uu = uu1"
shows "eqButUIDf (frds (uid := uu)) (frds1(uid := uu1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf (frds(uid := uu)) (frds1(uid := uu1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDf frds frds1
uid = UID1 \<Longrightarrow> eqButUIDl UID2 uu uu1
uid = UID2 \<Longrightarrow> eqButUIDl UID1 uu uu1
\<lbrakk>uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. eqButUIDf (frds(uid := uu)) (frds1(uid := uu1))
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)
uid = UID1 \<Longrightarrow> eqButUIDl UID2 uu uu1
uid = UID2 \<Longrightarrow> eqButUIDl UID1 uu uu1
\<lbrakk>uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. eqButUIDl UID2 ((frds(uid := uu)) UID1) ((frds1(uid := uu1)) UID1) \<and> eqButUIDl UID1 ((frds(uid := uu)) UID2) ((frds1(uid := uu1)) UID2) \<and> (\<forall>uida. uida \<noteq> UID1 \<and> uida \<noteq> UID2 \<longrightarrow> (frds(uid := uu)) uida = (frds1(uid := uu1)) uida)
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUIDf_eqButUIDl:
assumes "eqButUIDf frds frds1"
shows "eqButUIDl UID2 (frds UID1) (frds1 UID1)"
  and "eqButUIDl UID1 (frds UID2) (frds1 UID2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds1 UID1) &&& eqButUIDl UID1 (frds UID2) (frds1 UID2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDf frds frds1

goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds1 UID1) &&& eqButUIDl UID1 (frds UID2) (frds1 UID2)
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)

goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds1 UID1) &&& eqButUIDl UID1 (frds UID2) (frds1 UID2)
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUIDf_not_UID:
"\<lbrakk>eqButUIDf frds frds1; uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> frds uid = frds1 uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqButUIDf frds frds1; uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> frds uid = frds1 uid
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid); uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> frds uid = frds1 uid
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUIDf_not_UID':
assumes eq1: "eqButUIDf frds frds1"
and uid: "(uid,uid') \<notin> {(UID1,UID2), (UID2,UID1)}"
shows "uid \<in>\<in> frds uid' \<longleftrightarrow> uid \<in>\<in> frds1 uid'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
from uid
[PROOF STATE]
proof (chain)
picking this:
(uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)}
[PROOF STEP]
have "(uid' = UID1 \<and> uid \<noteq> UID2)
               \<or> (uid' = UID2 \<and> uid \<noteq> UID1)
               \<or> (uid' \<notin> {UID1,UID2})" (is "?u1 \<or> ?u2 \<or> ?n12")
[PROOF STATE]
proof (prove)
using this:
(uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)}

goal (1 subgoal):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<or> uid' = UID2 \<and> uid \<noteq> UID1 \<or> uid' \<notin> {UID1, UID2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uid' = UID1 \<and> uid \<noteq> UID2 \<or> uid' = UID2 \<and> uid \<noteq> UID1 \<or> uid' \<notin> {UID1, UID2}

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' = UID1 \<and> uid \<noteq> UID2 \<or> uid' = UID2 \<and> uid \<noteq> UID1 \<or> uid' \<notin> {UID1, UID2}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2 \<or> uid' = UID2 \<and> uid \<noteq> UID1 \<or> uid' \<notin> {UID1, UID2}

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 3. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
assume "?u1"
[PROOF STATE]
proof (state)
this:
uid' = UID1 \<and> uid \<noteq> UID2

goal (3 subgoals):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 3. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
uid' = UID1 \<and> uid \<noteq> UID2

goal (3 subgoals):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 3. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' = UID1 \<and> uid \<noteq> UID2
[PROOF STEP]
have "uid \<in>\<in> remove1 UID2 (frds uid') \<longleftrightarrow> uid \<in>\<in> remove1 UID2 (frds1 uid')"
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2
eqButUIDf frds frds1

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))

goal (3 subgoals):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 3. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
uid' = UID1 \<and> uid \<noteq> UID2
(uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2
(uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')

goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
assume "?u2"
[PROOF STATE]
proof (state)
this:
uid' = UID2 \<and> uid \<noteq> UID1

goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
uid' = UID2 \<and> uid \<noteq> UID1

goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' = UID2 \<and> uid \<noteq> UID1
[PROOF STEP]
have "uid \<in>\<in> remove1 UID1 (frds uid') \<longleftrightarrow> uid \<in>\<in> remove1 UID1 (frds1 uid')"
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<and> uid \<noteq> UID1

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<and> uid \<noteq> UID1
eqButUIDf frds frds1

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<and> uid \<noteq> UID1
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))

goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
uid' = UID2 \<and> uid \<noteq> UID1
(uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<and> uid \<noteq> UID1
(uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')

goal (1 subgoal):
 1. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
assume "?n12"
[PROOF STATE]
proof (state)
this:
uid' \<notin> {UID1, UID2}

goal (1 subgoal):
 1. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' \<notin> {UID1, UID2}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uid' \<notin> {UID1, UID2}

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
uid' \<notin> {UID1, UID2}
eqButUIDf frds frds1

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
uid' \<notin> {UID1, UID2}
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUID12_eeq[simp,intro!]: "eqButUID12 freq freq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 freq freq
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq uid uid'
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUID12_sym:
assumes "eqButUID12 freq freq1" shows "eqButUID12 freq1 freq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 freq1 freq
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUID12 freq freq1

goal (1 subgoal):
 1. eqButUID12 freq1 freq
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
using this:
\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq1 uid uid'

goal (1 subgoal):
 1. \<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq1 uid uid' = freq uid uid'
[PROOF STEP]
by presburger


[STATEMENT]
lemma eqButUID12_trans:
assumes "eqButUID12 freq freq1" and "eqButUID12 freq1 freq2"
shows "eqButUID12 freq freq2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 freq freq2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUID12 freq freq1
eqButUID12 freq1 freq2

goal (1 subgoal):
 1. eqButUID12 freq freq2
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
using this:
\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq1 uid uid'
\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq1 uid uid' = freq2 uid uid'

goal (1 subgoal):
 1. \<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq2 uid uid'
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUID12_not_UID:
"\<lbrakk>eqButUID12 freq freq1; \<not> (uid,uid') \<in> {(UID1,UID2), (UID2,UID1)}\<rbrakk> \<Longrightarrow> freq uid uid' = freq1 uid uid'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqButUID12 freq freq1; (uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)}\<rbrakk> \<Longrightarrow> freq uid uid' = freq1 uid uid'
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq1 uid uid'; (uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)}\<rbrakk> \<Longrightarrow> freq uid uid' = freq1 uid uid'
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUID_refl[simp,intro!]: "eqButUID s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admin s = admin s \<and> pendingUReqs s = pendingUReqs s \<and> userReq s = userReq s \<and> userIDs s = userIDs s \<and> user s = user s \<and> pass s = pass s \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s) \<and> eqButUID12 (friendReq s) (friendReq s) \<and> eqButUIDf (friendIDs s) (friendIDs s) \<and> postIDs s = postIDs s \<and> admin s = admin s \<and> post s = post s \<and> owner s = owner s \<and> vis s = vis s
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUID_sym[sym]:
assumes "eqButUID s s1" shows "eqButUID s1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s1 s
[PROOF STEP]
using assms eqButUIDf_sym eqButUID12_sym
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
eqButUIDf ?frds ?frds1.0 \<Longrightarrow> eqButUIDf ?frds1.0 ?frds
eqButUID12 ?freq ?freq1.0 \<Longrightarrow> eqButUID12 ?freq1.0 ?freq

goal (1 subgoal):
 1. eqButUID s1 s
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
using this:
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis s1
eqButUIDf ?frds ?frds1.0 \<Longrightarrow> eqButUIDf ?frds1.0 ?frds
eqButUID12 ?freq ?freq1.0 \<Longrightarrow> eqButUID12 ?freq1.0 ?freq

goal (1 subgoal):
 1. admin s1 = admin s \<and> pendingUReqs s1 = pendingUReqs s \<and> userReq s1 = userReq s \<and> userIDs s1 = userIDs s \<and> user s1 = user s \<and> pass s1 = pass s \<and> eqButUIDf (pendingFReqs s1) (pendingFReqs s) \<and> eqButUID12 (friendReq s1) (friendReq s) \<and> eqButUIDf (friendIDs s1) (friendIDs s) \<and> postIDs s1 = postIDs s \<and> admin s1 = admin s \<and> post s1 = post s \<and> owner s1 = owner s \<and> vis s1 = vis s
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUID_trans[trans]:
assumes "eqButUID s s1" and "eqButUID s1 s2" shows "eqButUID s s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s2
[PROOF STEP]
using assms eqButUIDf_trans eqButUID12_trans
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
eqButUID s1 s2
\<lbrakk>eqButUIDf ?frds ?frds1.0; eqButUIDf ?frds1.0 ?frds2.0\<rbrakk> \<Longrightarrow> eqButUIDf ?frds ?frds2.0
\<lbrakk>eqButUID12 ?freq ?freq1.0; eqButUID12 ?freq1.0 ?freq2.0\<rbrakk> \<Longrightarrow> eqButUID12 ?freq ?freq2.0

goal (1 subgoal):
 1. eqButUID s s2
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
using this:
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis s1
admin s1 = admin s2 \<and> pendingUReqs s1 = pendingUReqs s2 \<and> userReq s1 = userReq s2 \<and> userIDs s1 = userIDs s2 \<and> user s1 = user s2 \<and> pass s1 = pass s2 \<and> eqButUIDf (pendingFReqs s1) (pendingFReqs s2) \<and> eqButUID12 (friendReq s1) (friendReq s2) \<and> eqButUIDf (friendIDs s1) (friendIDs s2) \<and> postIDs s1 = postIDs s2 \<and> admin s1 = admin s2 \<and> post s1 = post s2 \<and> owner s1 = owner s2 \<and> vis s1 = vis s2
\<lbrakk>eqButUIDf ?frds ?frds1.0; eqButUIDf ?frds1.0 ?frds2.0\<rbrakk> \<Longrightarrow> eqButUIDf ?frds ?frds2.0
\<lbrakk>eqButUID12 ?freq ?freq1.0; eqButUID12 ?freq1.0 ?freq2.0\<rbrakk> \<Longrightarrow> eqButUID12 ?freq ?freq2.0

goal (1 subgoal):
 1. admin s = admin s2 \<and> pendingUReqs s = pendingUReqs s2 \<and> userReq s = userReq s2 \<and> userIDs s = userIDs s2 \<and> user s = user s2 \<and> pass s = pass s2 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s2) \<and> eqButUID12 (friendReq s) (friendReq s2) \<and> eqButUIDf (friendIDs s) (friendIDs s2) \<and> postIDs s = postIDs s2 \<and> admin s = admin s2 \<and> post s = post s2 \<and> owner s = owner s2 \<and> vis s = vis s2
[PROOF STEP]
by metis