[STATEMENT]
lemma "test (do {
  tmp0 \<leftarrow> Document_adoptNode_document . getElementsByTagName(''x<'');
  y \<leftarrow> return (tmp0 ! 0);
  child \<leftarrow> y . firstChild;
  tmp1 \<leftarrow> y . parentNode;
  tmp2 \<leftarrow> Document_adoptNode_document . body;
  assert_equals(tmp1, tmp2);
  tmp3 \<leftarrow> y . ownerDocument;
  assert_equals(tmp3, Document_adoptNode_document);
  tmp4 \<leftarrow> Document_adoptNode_document . adoptNode(y);
  assert_equals(tmp4, y);
  tmp5 \<leftarrow> y . parentNode;
  assert_equals(tmp5, None);
  tmp6 \<leftarrow> y . firstChild;
  assert_equals(tmp6, child);
  tmp7 \<leftarrow> y . ownerDocument;
  assert_equals(tmp7, Document_adoptNode_document);
  tmp8 \<leftarrow> child . ownerDocument;
  assert_equals(tmp8, Document_adoptNode_document);
  doc \<leftarrow> createDocument(None, None, None);
  tmp9 \<leftarrow> doc . adoptNode(y);
  assert_equals(tmp9, y);
  tmp10 \<leftarrow> y . parentNode;
  assert_equals(tmp10, None);
  tmp11 \<leftarrow> y . firstChild;
  assert_equals(tmp11, child);
  tmp12 \<leftarrow> y . ownerDocument;
  assert_equals(tmp12, doc);
  tmp13 \<leftarrow> child . ownerDocument;
  assert_equals(tmp13, doc)
}) Document_adoptNode_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind Document_adoptNode_document . getElementsByTagName(''x<'') (\<lambda>tmp0. Heap_Error_Monad.bind (return (tmp0 ! 0)) (\<lambda>y. Heap_Error_Monad.bind y . firstChild (\<lambda>child. Heap_Error_Monad.bind y . parentNode (\<lambda>tmp1. Heap_Error_Monad.bind Document_adoptNode_document . body (\<lambda>tmp2. Heap_Error_Monad.bind assert_array_equals(tmp1, tmp2) (\<lambda>_. Heap_Error_Monad.bind y . ownerDocument (\<lambda>tmp3. Heap_Error_Monad.bind assert_array_equals(tmp3, Document_adoptNode_document) (\<lambda>_. Heap_Error_Monad.bind Document_adoptNode_document . adoptNode(y) (\<lambda>tmp4. Heap_Error_Monad.bind assert_array_equals(tmp4, y) (\<lambda>_. Heap_Error_Monad.bind y . parentNode (\<lambda>tmp5. Heap_Error_Monad.bind assert_array_equals(tmp5, None) (\<lambda>_. Heap_Error_Monad.bind y . firstChild (\<lambda>tmp6. Heap_Error_Monad.bind assert_array_equals(tmp6, child) (\<lambda>_. Heap_Error_Monad.bind y . ownerDocument (\<lambda>tmp7. Heap_Error_Monad.bind assert_array_equals(tmp7, Document_adoptNode_document) (\<lambda>_. Heap_Error_Monad.bind child . ownerDocument (\<lambda>tmp8. Heap_Error_Monad.bind assert_array_equals(tmp8, Document_adoptNode_document) (\<lambda>_. Heap_Error_Monad.bind createDocument([]) (\<lambda>doc. Heap_Error_Monad.bind doc . adoptNode(y) (\<lambda>tmp9. Heap_Error_Monad.bind assert_array_equals(tmp9, y) (\<lambda>_. Heap_Error_Monad.bind y . parentNode (\<lambda>tmp10. Heap_Error_Monad.bind assert_array_equals(tmp10, None) (\<lambda>_. Heap_Error_Monad.bind y . firstChild (\<lambda>tmp11. Heap_Error_Monad.bind assert_array_equals(tmp11, child) (\<lambda>_. Heap_Error_Monad.bind y . ownerDocument (\<lambda>tmp12. Heap_Error_Monad.bind assert_array_equals(tmp12, doc) (\<lambda>_. Heap_Error_Monad.bind child . ownerDocument (\<lambda>tmp13. assert_array_equals(tmp13, doc)))))))))))))))))))))))))))))) Document_adoptNode_heap
[PROOF STEP]
by eval


[STATEMENT]
lemma "test (do {
  x \<leftarrow> Document_adoptNode_document . createElement('':good:times:'');
  tmp0 \<leftarrow> Document_adoptNode_document . adoptNode(x);
  assert_equals(tmp0, x);
  doc \<leftarrow> createDocument(None, None, None);
  tmp1 \<leftarrow> doc . adoptNode(x);
  assert_equals(tmp1, x);
  tmp2 \<leftarrow> x . parentNode;
  assert_equals(tmp2, None);
  tmp3 \<leftarrow> x . ownerDocument;
  assert_equals(tmp3, doc)
}) Document_adoptNode_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind Document_adoptNode_document . createElement('':good:times:'') (\<lambda>x. Heap_Error_Monad.bind Document_adoptNode_document . adoptNode(x) (\<lambda>tmp0. Heap_Error_Monad.bind assert_array_equals(tmp0, x) (\<lambda>_. Heap_Error_Monad.bind createDocument([]) (\<lambda>doc. Heap_Error_Monad.bind doc . adoptNode(x) (\<lambda>tmp1. Heap_Error_Monad.bind assert_array_equals(tmp1, x) (\<lambda>_. Heap_Error_Monad.bind x . parentNode (\<lambda>tmp2. Heap_Error_Monad.bind assert_array_equals(tmp2, None) (\<lambda>_. Heap_Error_Monad.bind x . ownerDocument (\<lambda>tmp3. assert_array_equals(tmp3, doc))))))))))) Document_adoptNode_heap
[PROOF STEP]
by eval


[STATEMENT]
lemma simple_rule_dtor_ids:
    "uncurry SimpleRule \<circ> simple_rule_dtor = id"
    "simple_rule_dtor \<circ> uncurry SimpleRule = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uncurry SimpleRule \<circ> simple_rule_dtor = id &&& simple_rule_dtor \<circ> uncurry SimpleRule = id
[PROOF STEP]
unfolding simple_rule_dtor_def comp_def fun_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. uncurry SimpleRule (case x of SimpleRule x xa \<Rightarrow> (x, xa)) = id x &&& \<forall>x. (case uncurry SimpleRule x of SimpleRule x xa \<Rightarrow> (x, xa)) = id x
[PROOF STEP]
by(simp_all split: simple_rule.splits)


[STATEMENT]
lemma evaluate_list_total0:
  fixes s :: "'a state"
  assumes "\<And>e env s'::'a state. e \<in> set es \<Longrightarrow> clock s' \<le> clock s \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)"
  shows "\<exists>s' r. evaluate_list True env s es (s', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_list True env s es (s', r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?e \<in> set es; clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate_list True env s es (s', r)
[PROOF STEP]
proof (induction es arbitrary: env s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set []; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s [] (s', r)
 2. \<And>a es env s. \<lbrakk>\<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s es (s', r); \<And>e s' env. \<lbrakk>e \<in> set (a # es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_list True env s (a # es) (s', r)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<lbrakk>?e \<in> set []; clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)

goal (2 subgoals):
 1. \<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set []; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s [] (s', r)
 2. \<And>a es env s. \<lbrakk>\<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s es (s', r); \<And>e s' env. \<lbrakk>e \<in> set (a # es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_list True env s (a # es) (s', r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_list True env s [] (s', r)
[PROOF STEP]
by (metis evaluate_match_evaluate_list_evaluate.empty)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_list True env s [] (s', r)

goal (1 subgoal):
 1. \<And>a es env s. \<lbrakk>\<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s es (s', r); \<And>e s' env. \<lbrakk>e \<in> set (a # es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_list True env s (a # es) (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a es env s. \<lbrakk>\<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s es (s', r); \<And>e s' env. \<lbrakk>e \<in> set (a # es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_list True env s (a # es) (s', r)
[PROOF STEP]
case (Cons e es)
[PROOF STATE]
proof (state)
this:
(\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock ?s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True ?env ?s es (s', r)
\<lbrakk>?e \<in> set (e # es); clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)

goal (1 subgoal):
 1. \<And>a es env s. \<lbrakk>\<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s es (s', r); \<And>e s' env. \<lbrakk>e \<in> set (a # es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_list True env s (a # es) (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock ?s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True ?env ?s es (s', r)
\<lbrakk>?e \<in> set (e # es); clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)
[PROOF STEP]
obtain s' r where e: "evaluate True env s e (s', r)"
[PROOF STATE]
proof (prove)
using this:
(\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock ?s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True ?env ?s es (s', r)
\<lbrakk>?e \<in> set (e # es); clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)

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

goal (1 subgoal):
 1. \<And>a es env s. \<lbrakk>\<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s es (s', r); \<And>e s' env. \<lbrakk>e \<in> set (a # es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_list True env s (a # es) (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e (s', r)
[PROOF STEP]
have clock: "clock s' \<le> clock s"
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e (s', r)

goal (1 subgoal):
 1. clock s' \<le> clock s
[PROOF STEP]
by (metis evaluate_clock_mono)
[PROOF STATE]
proof (state)
this:
clock s' \<le> clock s

goal (1 subgoal):
 1. \<And>a es env s. \<lbrakk>\<And>env s. (\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True env s es (s', r); \<And>e s' env. \<lbrakk>e \<in> set (a # es); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_list True env s (a # es) (s', r)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
case (Rval v)
[PROOF STATE]
proof (state)
this:
r = Rval v

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
have "\<exists>s'' r. evaluate_list True env s' es (s'', r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s'' r. evaluate_list True env s' es (s'', r)
[PROOF STEP]
using Cons clock
[PROOF STATE]
proof (prove)
using this:
(\<And>e s' env. \<lbrakk>e \<in> set es; clock s' \<le> clock ?s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_list True ?env ?s es (s', r)
\<lbrakk>?e \<in> set (e # es); clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)
clock s' \<le> clock s

goal (1 subgoal):
 1. \<exists>s'' r. evaluate_list True env s' es (s'', r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>s'' r. evaluate_list True env s' es (s'', r)

goal (2 subgoals):
 1. \<And>x1. r = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
 2. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s'' r. evaluate_list True env s' es (s'', r)
[PROOF STEP]
obtain s'' r where "evaluate_list True env s' es (s'', r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s'' r. evaluate_list True env s' es (s'', r)

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

goal (2 subgoals):
 1. \<And>x1. r__ = Rval x1 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
 2. \<And>x2. r__ = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
with e Rval
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e (s', r__)
r__ = Rval v
evaluate_list True env s' es (s'', r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e (s', r__)
r__ = Rval v
evaluate_list True env s' es (s'', r)

goal (1 subgoal):
 1. \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
by (cases r)
           (metis evaluate_match_evaluate_list_evaluate.cons1 evaluate_match_evaluate_list_evaluate.cons3)+
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_list True env s (e # es) (s', r)

goal (1 subgoal):
 1. \<And>x2. r__ = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
case Rerr
[PROOF STATE]
proof (state)
this:
r = Rerr x2_

goal (1 subgoal):
 1. \<And>x2. r = Rerr x2 \<Longrightarrow> \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
with e
[PROOF STATE]
proof (chain)
picking this:
evaluate True env s e (s', r)
r = Rerr x2_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
evaluate True env s e (s', r)
r = Rerr x2_

goal (1 subgoal):
 1. \<exists>s' r. evaluate_list True env s (e # es) (s', r)
[PROOF STEP]
by (metis evaluate_match_evaluate_list_evaluate.cons2)
[PROOF STATE]
proof (state)
this:
\<exists>s' r. evaluate_list True env s (e # es) (s', r)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma evaluate_match_total0:
  fixes s :: "'a state"
  assumes "\<And>p e env s'::'a state. (p, e) \<in> set pes \<Longrightarrow> clock s' \<le> clock s \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)"
  shows "\<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]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?p, ?e) \<in> set pes; clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)

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. (\<And>p e s' env. \<lbrakk>(p, e) \<in> set []; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v [] v' (s', r)
 2. \<And>a pes env s. \<lbrakk>\<And>env s. (\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v pes v' (s', r); \<And>p e s' env. \<lbrakk>(p, e) \<in> set (a # pes); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (a # pes) v' (s', r)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?p, ?e) \<in> set []; clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)

goal (2 subgoals):
 1. \<And>env s. (\<And>p e s' env. \<lbrakk>(p, e) \<in> set []; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v [] v' (s', r)
 2. \<And>a pes env s. \<lbrakk>\<And>env s. (\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v pes v' (s', r); \<And>p e s' env. \<lbrakk>(p, e) \<in> set (a # pes); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<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. \<lbrakk>\<And>env s. (\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v pes v' (s', r); \<And>p e s' env. \<lbrakk>(p, e) \<in> set (a # pes); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<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. \<lbrakk>\<And>env s. (\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v pes v' (s', r); \<And>p e s' env. \<lbrakk>(p, e) \<in> set (a # pes); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<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:
(\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock ?s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True ?env ?s v pes v' (s', r)
\<lbrakk>(?p, ?e) \<in> set (pe # pes); clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)

goal (1 subgoal):
 1. \<And>a pes env s. \<lbrakk>\<And>env s. (\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v pes v' (s', r); \<And>p e s' env. \<lbrakk>(p, e) \<in> set (a # pes); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<Longrightarrow> \<exists>s' r. evaluate_match True env s v (a # pes) v' (s', r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock ?s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True ?env ?s v pes v' (s', r)
\<lbrakk>(?p, ?e) \<in> set (pe # pes); clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (s'', r)
[PROOF STEP]
obtain p e where "pe = (p, e)"
[PROOF STATE]
proof (prove)
using this:
(\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock ?s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True ?env ?s v pes v' (s', r)
\<lbrakk>(?p, ?e) \<in> set (pe # pes); clock ?s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True ?env ?s' ?e (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. \<lbrakk>\<And>env s. (\<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)) \<Longrightarrow> \<exists>s' r. evaluate_match True env s v pes v' (s', r); \<And>p e s' env. \<lbrakk>(p, e) \<in> set (a # pes); clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)\<rbrakk> \<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]
apply (rule Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> \<exists>s'' r. evaluate True env s' e (s'', r)
[PROOF STEP]
apply (rule Cons)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> (?p2 p e s' env, e) \<in> set (pe # pes)
 2. \<And>p e s' env. \<lbrakk>(p, e) \<in> set pes; clock s' \<le> clock s\<rbrakk> \<Longrightarrow> clock s' \<le> clock s
[PROOF STEP]
by auto
[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]
apply (rule Cons)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (?p, e) \<in> set (pe # pes)
 2. clock s \<le> clock s
[PROOF STEP]
unfolding \<open>pe = _\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (?p, e) \<in> set ((p, e) # pes)
 2. clock s \<le> clock s
[PROOF STEP]
by auto
[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