[STATEMENT]
lemma get_child_nodes_pure [simp]:
  "pure (get_child_nodes ptr) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure (get_child_nodes ptr) h
[PROOF STEP]
unfolding get_child_nodes_def a_get_child_nodes_tups_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure (invoke (CD.a_get_child_nodes_tups @ [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r, get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)]) ptr ()) h
[PROOF STEP]
proof(split CD.get_child_nodes_splits, rule conjI; clarify)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr \<Longrightarrow> pure (get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr) h
 2. \<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr \<Longrightarrow> pure (invoke [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r, get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)] ptr ()) h
[PROOF STEP]
assume "known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr"
[PROOF STATE]
proof (state)
this:
known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr

goal (2 subgoals):
 1. known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr \<Longrightarrow> pure (get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr) h
 2. \<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr \<Longrightarrow> pure (invoke [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r, get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)] ptr ()) h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr
[PROOF STEP]
show "pure (get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr) h"
[PROOF STATE]
proof (prove)
using this:
known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr

goal (1 subgoal):
 1. pure (get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr) h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pure (get_child_nodes\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr) h

goal (1 subgoal):
 1. \<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr \<Longrightarrow> pure (invoke [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r, get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)] ptr ()) h
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr \<Longrightarrow> pure (invoke [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r, get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)] ptr ()) h
[PROOF STEP]
assume "\<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr"
[PROOF STATE]
proof (state)
this:
\<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr

goal (1 subgoal):
 1. \<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr \<Longrightarrow> pure (invoke [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r, get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)] ptr ()) h
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr
[PROOF STEP]
show "pure (invoke [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r,
       get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)]
     ptr ()) h"
[PROOF STATE]
proof (prove)
using this:
\<not> known_ptr\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M ptr

goal (1 subgoal):
 1. pure (invoke [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r, get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)] ptr ()) h
[PROOF STEP]
by(auto simp add: get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def intro: bind_pure_I split: invoke_splits)
[PROOF STATE]
proof (state)
this:
pure (invoke [(is_shadow_root_ptr\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r, get_child_nodes\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r \<circ> the \<circ> cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r)] ptr ()) h

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Rep_uint16'_code [code]: "Rep_uint16' x = (BITS n. bit x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_uint16' x = (BITS n. bit x n)
[PROOF STEP]
by transfer (simp add: set_bits_bit_eq)


[STATEMENT]
lemma PO_refines_implies_Range_invariant:
  "PO_refines R Ta Tc \<Longrightarrow> reach Tc \<subseteq> Range R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PO_refines R Ta Tc \<Longrightarrow> reach Tc \<subseteq> Range R
[PROOF STEP]
by (rule INV_rule)
   (auto intro!: PO_refines_implies_Range_init
                 PO_refines_implies_Range_trans)


[STATEMENT]
lemma variance_divide:
  fixes f :: "'a \<Rightarrow> real"
  assumes "integrable M f"
  shows "variance (\<lambda>\<omega>. f \<omega> / r) = variance f / r^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. expectation (\<lambda>x. (f x / r - expectation (\<lambda>\<omega>. f \<omega> / r))\<^sup>2) = expectation (\<lambda>x. (f x - expectation f)\<^sup>2) / r\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
integrable M f

goal (1 subgoal):
 1. expectation (\<lambda>x. (f x / r - expectation (\<lambda>\<omega>. f \<omega> / r))\<^sup>2) = expectation (\<lambda>x. (f x - expectation f)\<^sup>2) / r\<^sup>2
[PROOF STEP]
by (subst Bochner_Integration.integral_divide[OF assms(1)])
    (simp add:diff_divide_distrib[symmetric] power2_eq_square algebra_simps)


[STATEMENT]
lemma OclANY_null[simp,code_unfold]:"(null->any\<^sub>S\<^sub>e\<^sub>t()) = null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. null->any\<^sub>S\<^sub>e\<^sub>t() = null
[PROOF STEP]
by(simp add: OclANY_def false_def true_def)


[STATEMENT]
lemma sparsegrid'I[intro]:
  assumes b: "b \<in> sparsegrid' dm" and p: "p \<in> grid b ds"
  shows "p \<in> sparsegrid' dm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> sparsegrid' dm
[PROOF STEP]
using sparsegrid'_length[OF b] b
       grid_transitive[OF grid_subset_alldim[OF p], where c="start dm" and ds''="{0..<dm}"]
[PROOF STATE]
proof (prove)
using this:
length b = dm
b \<in> sparsegrid' dm
\<lbrakk>b \<in> grid (start dm) ?ds'; ?ds' \<subseteq> {0..<dm}; {0..<length b} \<subseteq> {0..<dm}\<rbrakk> \<Longrightarrow> p \<in> grid (start dm) {0..<dm}

goal (1 subgoal):
 1. p \<in> sparsegrid' dm
[PROOF STEP]
unfolding sparsegrid'_def
[PROOF STATE]
proof (prove)
using this:
length b = dm
b \<in> grid (start dm) {0..<dm}
\<lbrakk>b \<in> grid (start dm) ?ds'; ?ds' \<subseteq> {0..<dm}; {0..<length b} \<subseteq> {0..<dm}\<rbrakk> \<Longrightarrow> p \<in> grid (start dm) {0..<dm}

goal (1 subgoal):
 1. p \<in> grid (start dm) {0..<dm}
[PROOF STEP]
by auto


[STATEMENT]
lemma valuate_with_dim_poly: "z \<lbrace> X \<rbrace> = (\<Sum>i\<in>{0..<dim_poly z}. coeff z i * X i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<lbrace> X \<rbrace> = (\<Sum>i = 0..<dim_poly z. Abstract_Linear_Poly.coeff z i * X i)
[PROOF STEP]
using eval_poly_with_sum_superset[of "{0..<dim_poly z}" z X]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {0..<dim_poly z}; vars z \<subseteq> {0..<dim_poly z}\<rbrakk> \<Longrightarrow> z \<lbrace> X \<rbrace> = (\<Sum>x = 0..<dim_poly z. Abstract_Linear_Poly.coeff z x * X x)

goal (1 subgoal):
 1. z \<lbrace> X \<rbrace> = (\<Sum>i = 0..<dim_poly z. Abstract_Linear_Poly.coeff z i * X i)
[PROOF STEP]
using vars_subset_0_dim_poly
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite {0..<dim_poly z}; vars z \<subseteq> {0..<dim_poly z}\<rbrakk> \<Longrightarrow> z \<lbrace> X \<rbrace> = (\<Sum>x = 0..<dim_poly z. Abstract_Linear_Poly.coeff z x * X x)
vars ?z \<subseteq> {0..<dim_poly ?z}

goal (1 subgoal):
 1. z \<lbrace> X \<rbrace> = (\<Sum>i = 0..<dim_poly z. Abstract_Linear_Poly.coeff z i * X i)
[PROOF STEP]
by blast


[STATEMENT]
lemma start_addrs_NewHeapElem_start_heap_obsD:
  "a \<in> set start_addrs \<Longrightarrow> \<exists>CTn. NewHeapElem a CTn \<in> set start_heap_obs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> set start_addrs \<Longrightarrow> \<exists>CTn. NewHeapElem a CTn \<in> set start_heap_obs
[PROOF STEP]
using length_initialization_list_le_length_start_addrs
[PROOF STATE]
proof (prove)
using this:
length start_addrs \<le> length initialization_list

goal (1 subgoal):
 1. a \<in> set start_addrs \<Longrightarrow> \<exists>CTn. NewHeapElem a CTn \<in> set start_heap_obs
[PROOF STEP]
unfolding start_heap_obs_def start_addrs_def
[PROOF STATE]
proof (prove)
using this:
length (fst (snd start_heap_data)) \<le> length initialization_list

goal (1 subgoal):
 1. a \<in> set (fst (snd start_heap_data)) \<Longrightarrow> \<exists>CTn. NewHeapElem a CTn \<in> set (map2 (\<lambda>C a. NewHeapElem a (Class_type C)) initialization_list (fst (snd start_heap_data)))
[PROOF STEP]
by(force simp add: set_zip in_set_conv_nth intro: rev_image_eqI)


[STATEMENT]
lemma to_ordered_collection_det:
  "to_ordered_collection \<tau> \<sigma>\<^sub>1 \<Longrightarrow>
   to_ordered_collection \<tau> \<sigma>\<^sub>2 \<Longrightarrow> \<sigma>\<^sub>1 = \<sigma>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>to_ordered_collection \<tau> \<sigma>\<^sub>1; to_ordered_collection \<tau> \<sigma>\<^sub>2\<rbrakk> \<Longrightarrow> \<sigma>\<^sub>1 = \<sigma>\<^sub>2
[PROOF STEP]
by (induct rule: to_ordered_collection.induct; simp add: to_ordered_collection.simps)


[STATEMENT]
lemma struct_specI:
  assumes "sel_spec sel" and "ap_spec ap" and "ab_spec ab" and "compl_struct compl"
  shows "struct_spec sel ap ab compl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. struct_spec sel ap ab compl
[PROOF STEP]
unfolding struct_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sel_spec sel \<and> ap_spec ap \<and> ab_spec ab \<and> compl_struct compl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sel_spec sel
ap_spec ap
ab_spec ab
compl_struct compl

goal (1 subgoal):
 1. sel_spec sel \<and> ap_spec ap \<and> ab_spec ab \<and> compl_struct compl
[PROOF STEP]
by (intro conjI)


[STATEMENT]
theorem gb_schema_direct_pmdl:
  assumes "struct_spec sel ap ab compl" and "compl_pmdl compl"
  shows "pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)
[PROOF STEP]
have "pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) =
          pmdl (fst ` set ([] @ (fst (add_indices (bs, data) (0, data)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))
[PROOF STEP]
unfolding fst_gb_schema_direct Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_aux sel ap ab compl [] (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data) (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (ap [] [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)))) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
struct_spec sel ap ab compl
compl_pmdl compl

goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_aux sel ap ab compl [] (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data) (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (ap [] [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)))) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))
[PROOF STEP]
proof (rule gb_schema_aux_pmdl_init)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. is_Groebner_basis (fst ` set [])
 2. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 3. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
from is_Groebner_basis_empty
[PROOF STATE]
proof (chain)
picking this:
is_Groebner_basis {}
[PROOF STEP]
show "is_Groebner_basis (fst ` set [])"
[PROOF STATE]
proof (prove)
using this:
is_Groebner_basis {}

goal (1 subgoal):
 1. is_Groebner_basis (fst ` set [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_Groebner_basis (fst ` set [])

goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
let ?data = "(length bs, data)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
struct_spec sel ap ab compl
[PROOF STEP]
have "ab_spec ab"
[PROOF STATE]
proof (prove)
using this:
struct_spec sel ap ab compl

goal (1 subgoal):
 1. ab_spec ab
[PROOF STEP]
by (rule struct_specD)
[PROOF STATE]
proof (state)
this:
ab_spec ab

goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ab_spec ab

goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
have "unique_idx ([] @ []) (0, data)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unique_idx ([] @ []) (0, data)
[PROOF STEP]
by (simp add: unique_idx_Nil)
[PROOF STATE]
proof (state)
this:
unique_idx ([] @ []) (0, data)

goal (2 subgoals):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
 2. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ab_spec ab
unique_idx ([] @ []) (0, data)
[PROOF STEP]
show "unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) ?data) ?data"
[PROOF STATE]
proof (prove)
using this:
ab_spec ab
unique_idx ([] @ []) (0, data)

goal (1 subgoal):
 1. unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)
[PROOF STEP]
proof (rule unique_idx_ab)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices ?aux (0, data)
[PROOF STEP]
show "(fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices (bs, data) (0, data)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices (bs, data) (0, data)
[PROOF STEP]
by (simp add: add_indices_def)
[PROOF STATE]
proof (state)
this:
(fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices (bs, data) (0, data)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (length bs, data)

goal (1 subgoal):
 1. rem_comps_spec ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)) (count_rem_components (ab [] [] (fst (add_indices (bs, data) (0, data))) (length bs, data)), length bs, data)
[PROOF STEP]
qed (simp add: rem_comps_spec_count_rem_components)
[PROOF STATE]
proof (state)
this:
pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))

goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set ([] @ fst (add_indices (bs, data) (0, data))))

goal (1 subgoal):
 1. pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)
[PROOF STEP]
by (simp add: fst_set_add_indices)
[PROOF STATE]
proof (state)
this:
pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nextElem_append[simp]:
 "y \<notin> set xs \<Longrightarrow> nextElem (xs @ ys) d y = nextElem ys d y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> set xs \<Longrightarrow> nextElem (xs @ ys) d y = nextElem ys d y
[PROOF STEP]
by(induct xs) auto


[STATEMENT]
lemma nextElem_notin_butlast[rule_format,simp]:
 "y \<notin> set(butlast xs) \<longrightarrow> nextElem xs x y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> set (butlast xs) \<longrightarrow> nextElem xs x y = x
[PROOF STEP]
by(induct xs) auto


[STATEMENT]
lemma P16_invariant:
shows "invariant (composition) P16"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant composition P16
[PROOF STEP]
proof (rule invariantI, simp_all only:split_paired_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P16 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
fix s1 s2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P16 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
assume "(s1,s2) \<in> ioa.start (composition)"
[PROOF STATE]
proof (state)
this:
(s1, s2) \<in> ioa.start composition

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P16 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
thus "P16 (s1,s2)"
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<in> ioa.start composition

goal (1 subgoal):
 1. P16 (s1, s2)
[PROOF STEP]
using ids
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<in> ioa.start composition
0 < id1
id1 < id2

goal (1 subgoal):
 1. P16 (s1, s2)
[PROOF STEP]
by (auto simp add:comp_simps)
[PROOF STATE]
proof (state)
this:
P16 (s1, s2)

goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
fix s1 s2 t1 t2 a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
assume hyp: "P16 (s1,s2)" and trans:"(s1,s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1,t2)"
[PROOF STATE]
proof (state)
this:
P16 (s1, s2)
(s1, s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1, t2)

goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P16 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P16 (aa, ba)
[PROOF STEP]
show "P16 (t1,t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P16 (t1, t2)
[PROOF STEP]
using trans and hyp
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1, t2)
P16 (s1, s2)

goal (1 subgoal):
 1. P16 (t1, t2)
[PROOF STEP]
by (cases rule:trans_elim) auto
[PROOF STATE]
proof (state)
this:
P16 (t1, t2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P14_invariant:
shows "invariant (composition) P14"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant composition P14
[PROOF STEP]
proof (rule invariantI, simp_all only:split_paired_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P14 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P14 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P14 (aa, ba)
[PROOF STEP]
fix s1 s2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P14 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P14 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P14 (aa, ba)
[PROOF STEP]
assume "(s1,s2) \<in> ioa.start (composition)"
[PROOF STATE]
proof (state)
this:
(s1, s2) \<in> ioa.start composition

goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ioa.start composition \<Longrightarrow> P14 (a, b)
 2. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P14 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P14 (aa, ba)
[PROOF STEP]
thus "P14 (s1,s2)"
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<in> ioa.start composition

goal (1 subgoal):
 1. P14 (s1, s2)
[PROOF STEP]
using ids
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<in> ioa.start composition
0 < id1
id1 < id2

goal (1 subgoal):
 1. P14 (s1, s2)
[PROOF STEP]
by (auto simp add:comp_simps)
[PROOF STATE]
proof (state)
this:
P14 (s1, s2)

goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P14 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P14 (aa, ba)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P14 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P14 (aa, ba)
[PROOF STEP]
fix s1 s2 t1 t2 a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P14 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P14 (aa, ba)
[PROOF STEP]
assume hyp: "P14 (s1,s2)" and trans:"(s1,s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1,t2)"
[PROOF STATE]
proof (state)
this:
P14 (s1, s2)
(s1, s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1, t2)

goal (1 subgoal):
 1. \<And>a b aa ba ab. \<lbrakk>reachable composition (a, b); P14 (a, b); (a, b) \<midarrow>ab\<midarrow>composition\<longrightarrow> (aa, ba)\<rbrakk> \<Longrightarrow> P14 (aa, ba)
[PROOF STEP]
show "P14 (t1,t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P14 (t1, t2)
[PROOF STEP]
using trans and hyp
[PROOF STATE]
proof (prove)
using this:
(s1, s2) \<midarrow>a\<midarrow>composition\<longrightarrow> (t1, t2)
P14 (s1, s2)

goal (1 subgoal):
 1. P14 (t1, t2)
[PROOF STEP]
by (cases rule:trans_elim, auto simp add:safeInits_def)
[PROOF STATE]
proof (state)
this:
P14 (t1, t2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma my_trancl_step_induct [consumes 1, case_names base step]:
  "\<lbrakk>(a, b) \<in> r\<^sup>+;
   \<And>x y. (x, y) \<in> r \<Longrightarrow> P x y;
   \<And>x y z. P x y \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> r\<^sup>+; \<And>x y. (x, y) \<in> r \<Longrightarrow> P x y; \<And>x y z. \<lbrakk>P x y; (y, z) \<in> r\<rbrakk> \<Longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b
[PROOF STEP]
by (induct rule: trancl_induct, blast+)


[STATEMENT]
lemma multiple_t_wise_balance:
  assumes "n > 0"
  shows "t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
interpret des: proper_design \<V> "(multiple_blocks n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_design \<V> (multiple_blocks n)
[PROOF STEP]
by (simp add: assms multiple_proper_design)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
using t_non_zero t_lt_order multiple_t_wise_balance_index
[PROOF STATE]
proof (prove)
using this:
1 \<le> \<t>
\<t> \<le> des.\<v>
\<lbrakk>?ps \<subseteq> \<V>; card ?ps = \<t>\<rbrakk> \<Longrightarrow> multiple_blocks ?n index ?ps = \<Lambda>\<^sub>t * ?n

goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
by (unfold_locales) (simp_all)
[PROOF STATE]
proof (state)
this:
t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_indices_balanced: "point_indices \<t> = {\<Lambda>\<^sub>t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
have "point_indices \<t> = {i . \<exists> ps . i = \<B> index ps \<and> card ps = \<t> \<and> ps \<subseteq> \<V>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}
[PROOF STEP]
by (simp add: point_indices_def)
[PROOF STATE]
proof (state)
this:
point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}

goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}
[PROOF STEP]
have "point_indices  \<t> = {i . i = \<Lambda>\<^sub>t}"
[PROOF STATE]
proof (prove)
using this:
point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}

goal (1 subgoal):
 1. point_indices \<t> = {i. i = \<Lambda>\<^sub>t}
[PROOF STEP]
using balanced Collect_cong obtain_t_subset_points
[PROOF STATE]
proof (prove)
using this:
point_indices \<t> = {\<B> index ps |ps. card ps = \<t> \<and> ps \<subseteq> \<V>}
\<lbrakk>?ps \<subseteq> \<V>; card ?ps = \<t>\<rbrakk> \<Longrightarrow> \<B> index ?ps = \<Lambda>\<^sub>t
(\<And>x. ?P x = ?Q x) \<Longrightarrow> {x. ?P x} = {x. ?Q x}
(\<And>T. \<lbrakk>T \<subseteq> \<V>; card T = \<t>; finite T\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. point_indices \<t> = {i. i = \<Lambda>\<^sub>t}
[PROOF STEP]
by (smt (verit, best))
[PROOF STATE]
proof (state)
this:
point_indices \<t> = {i. i = \<Lambda>\<^sub>t}

goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
point_indices \<t> = {i. i = \<Lambda>\<^sub>t}

goal (1 subgoal):
 1. point_indices \<t> = {\<Lambda>\<^sub>t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
point_indices \<t> = {\<Lambda>\<^sub>t}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma match_sound:
  assumes "match t p = Some \<sigma>"
  shows "\<sigma> \<in> matchers {(p, t)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> \<in> matchers {(p, t)}
[PROOF STEP]
using match_list_sound [of Var "[(p, t)]"] and assms
[PROOF STATE]
proof (prove)
using this:
match_list Var [(p, t)] = Some ?\<sigma> \<Longrightarrow> ?\<sigma> \<in> matchers (set [(p, t)])
match t p = Some \<sigma>

goal (1 subgoal):
 1. \<sigma> \<in> matchers {(p, t)}
[PROOF STEP]
by (simp add: match_def)


[STATEMENT]
lemma tbisim_flip [flip_simps]:
  "FWbisimulation_base.tbisim (\<lambda>t. flip (bisim t)) (flip bisim_wait) w t ts2 m2 ts1 m1 =
   FWbisimulation_base.tbisim bisim bisim_wait w t ts1 m1 ts2 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWbisimulation_base.tbisim (\<lambda>t. flip (bisim t)) (flip bisim_wait) w t ts2 m2 ts1 m1 = FWbisimulation_base.tbisim bisim bisim_wait w t ts1 m1 ts2 m2
[PROOF STEP]
unfolding FWbisimulation_base.tbisim_def flip_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case ts2 of None \<Rightarrow> ts1 = None | \<lfloor>(x1, ln)\<rfloor> \<Rightarrow> \<exists>x2. ts1 = \<lfloor>(x2, ln)\<rfloor> \<and> bisim t (x2, m1) (x1, m2) \<and> (w \<or> bisim_wait x2 x1)) = (case ts1 of None \<Rightarrow> ts2 = None | \<lfloor>(x1, ln)\<rfloor> \<Rightarrow> \<exists>x2. ts2 = \<lfloor>(x2, ln)\<rfloor> \<and> bisim t (x1, m1) (x2, m2) \<and> (w \<or> bisim_wait x1 x2))
[PROOF STEP]
by auto


[STATEMENT]
lemma FWdelay_bisimulation_diverge_flip:
  "FWdelay_bisimulation_diverge final2 r2 final1 r1 (\<lambda>t. flip (bisim t)) (flip bisim_wait) \<tau>move2 \<tau>move1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge final2 r2 final1 r1 (\<lambda>t. flip (bisim t)) (flip bisim_wait) \<tau>move2 \<tau>move1
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. FWdelay_bisimulation_obs final2 r2 final1 r1 (\<lambda>t. flip (bisim t)) (flip bisim_wait) \<tau>move2 \<tau>move1
 2. FWdelay_bisimulation_diverge_axioms r2 r1 (\<lambda>t. flip (bisim t)) \<tau>move2 \<tau>move1
[PROOF STEP]
apply(rule FWdelay_bisimulation_obs_flip)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge_axioms r2 r1 (\<lambda>t. flip (bisim t)) \<tau>move2 \<tau>move1
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge_axioms.intro)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. delay_bisimulation_diverge (r2 t) (r1 t) (flip (bisim t)) (ta_bisim (\<lambda>t. flip (bisim t))) \<tau>move2 \<tau>move1
[PROOF STEP]
apply(unfold flip_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. delay_bisimulation_diverge (r1 t) (r2 t) (bisim t) ta_bisim_bisim_syntax \<tau>move1 \<tau>move2
[PROOF STEP]
apply(rule delay_bisimulation_diverge_axioms)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma closed_nlistsI:
  "closed S f \<Longrightarrow> closed (nlists n S) (map2 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed S f \<Longrightarrow> closed (nlists n S) (map2 f)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed S f \<Longrightarrow> closed (nlists n S) (map2 f)
[PROOF STEP]
apply (unfold closed_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S
[PROOF STEP]
apply (induct n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists 0 S. \<forall>y\<in>nlists 0 S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists 0 S
 2. \<And>n. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S\<rbrakk> \<Longrightarrow> \<forall>x\<in>nlists (Suc n) S. \<forall>y\<in>nlists (Suc n) S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists (Suc n) S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S\<rbrakk> \<Longrightarrow> \<forall>x\<in>nlists (Suc n) S. \<forall>y\<in>nlists (Suc n) S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists (Suc n) S
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S \<Longrightarrow> \<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; x \<in> nlists (Suc n) S; y \<in> nlists (Suc n) S\<rbrakk> \<Longrightarrow> x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists (Suc n) S
[PROOF STEP]
apply (simp add: in_nlists_Suc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; \<exists>y\<in>S. \<exists>ys\<in>nlists n S. x = y # ys; \<exists>ya\<in>S. \<exists>ys\<in>nlists n S. y = ya # ys\<rbrakk> \<Longrightarrow> \<exists>ya\<in>S. \<exists>ys\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y = ya # ys
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n x y ya yb ys ysa. \<lbrakk>\<forall>x\<in>nlists n S. \<forall>y\<in>nlists n S. x [\<squnion>\<^bsub>f\<^esub>] y \<in> nlists n S; \<forall>x\<in>S. \<forall>y\<in>S. x \<squnion>\<^bsub>f\<^esub> y \<in> S; ya \<in> S; yb \<in> S; ys \<in> nlists n S; ysa \<in> nlists n S\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. \<exists>ysb\<in>nlists n S. ya # ys [\<squnion>\<^bsub>f\<^esub>] (yb # ysa) = y # ysb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fds_abs_summable_zeta:
  "(s :: 'a :: {banach, nat_power_normed_field}) \<bullet> 1 > 1 \<Longrightarrow> fds_abs_converges fds_zeta s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < s \<bullet> (1::'a) \<Longrightarrow> fds_abs_converges fds_zeta s
[PROOF STEP]
by simp


[STATEMENT]
lemma list_map_autoref_update[autoref_rules]:
  assumes eq: "GEN_OP eq (=) (Rk\<rightarrow>Rk\<rightarrow>Id)"
  shows "(list_map_update eq, op_map_update) \<in>
      Rk \<rightarrow> Rv \<rightarrow> \<langle>Rk,Rv\<rangle>list_map_rel \<rightarrow> \<langle>Rk,Rv\<rangle>list_map_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_map_update eq, op_map_update) \<in> Rk \<rightarrow> Rv \<rightarrow> \<langle>Rk, Rv\<rangle>list_map_rel \<rightarrow> \<langle>Rk, Rv\<rangle>list_map_rel
[PROOF STEP]
unfolding list_map_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_map_update eq, op_map_update) \<in> Rk \<rightarrow> Rv \<rightarrow> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel O br map_of list_map_invar \<rightarrow> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel O br map_of list_map_invar
[PROOF STEP]
apply (intro fun_relI, elim relcompE, intro relcompI, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a a'b x y. \<lbrakk>(a, a') \<in> Rk; (aa, a'a) \<in> Rv; (x, y) \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; (y, a'b) \<in> br map_of list_map_invar\<rbrakk> \<Longrightarrow> (list_map_update eq a aa x, ?b4 a a' aa a'a x a'b x y a'b) \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel
 2. \<And>a a' aa a'a ab a'b x y z. \<lbrakk>(a, a') \<in> Rk; (aa, a'a) \<in> Rv; (ab, a'b) = (x, z); (x, y) \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; (y, z) \<in> br map_of list_map_invar\<rbrakk> \<Longrightarrow> (?b4 a a' aa a'a ab a'b x y z, op_map_update a' a'a a'b) \<in> br map_of list_map_invar
[PROOF STEP]
apply (erule (2) list_map_autoref_update1[param_fo, OF eq[simplified]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b x y z. \<lbrakk>(a, a') \<in> Rk; (aa, a'a) \<in> Rv; (ab, a'b) = (x, z); (x, y) \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; (y, z) \<in> br map_of list_map_invar\<rbrakk> \<Longrightarrow> (list_map_update (=) a' a'a y, op_map_update a' a'a a'b) \<in> br map_of list_map_invar
[PROOF STEP]
apply (rule list_map_autoref_update2[param_fo], simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma jmm_start_heap_ok: "jmm.start_heap_ok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jmm'.start_heap_ok
[PROOF STEP]
apply(simp add: jmm.start_heap_ok_def jmm.start_heap_data_def initialization_list_def sys_xcpts_list_def jmm.create_initial_object_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jmm_allocate jmm_empty (Class_type Thread) \<noteq> {} \<and> (jmm_allocate jmm_empty (Class_type Thread) \<noteq> {} \<longrightarrow> snd (snd (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (case SOME ha. ha \<in> jmm_allocate jmm_empty (Class_type Thread) of (h', a'') \<Rightarrow> (h', [a''], True)) NullPointer) ClassCast) OutOfMemory) ArrayIndexOutOfBounds) ArrayStore) NegativeArraySize) ArithmeticException) IllegalMonitorState) IllegalThreadState) InterruptedException)))
[PROOF STEP]
apply(split prod.split, clarify, clarsimp simp add: jmm.create_initial_object_simps jmm_allocate_eq_empty Thread_neq_sys_xcpts sys_xcpts_neqs dest!: jmm_allocate_Eps jmm_allocate_otherD)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rtrancl3p_induct1:
  "\<lbrakk> rtrancl3p r a bs c; P a; \<And>bs c b d. \<lbrakk> rtrancl3p r a bs c; r c b d; P c \<rbrakk> \<Longrightarrow> P d \<rbrakk> \<Longrightarrow> P c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rtrancl3p r a bs c; P a; \<And>bs c b d. \<lbrakk>rtrancl3p r a bs c; r c b d; P c\<rbrakk> \<Longrightarrow> P d\<rbrakk> \<Longrightarrow> P c
[PROOF STEP]
apply(induct rule: rtrancl3p.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>P a; \<And>bs c b d. \<lbrakk>rtrancl3p r a bs c; r c b d; P c\<rbrakk> \<Longrightarrow> P d\<rbrakk> \<Longrightarrow> P a
 2. \<And>a bs a' b a''. \<lbrakk>rtrancl3p r a bs a'; \<lbrakk>P a; \<And>bs c b d. \<lbrakk>rtrancl3p r a bs c; r c b d; P c\<rbrakk> \<Longrightarrow> P d\<rbrakk> \<Longrightarrow> P a'; r a' b a''; P a; \<And>bs c b d. \<lbrakk>rtrancl3p r a bs c; r c b d; P c\<rbrakk> \<Longrightarrow> P d\<rbrakk> \<Longrightarrow> P a''
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma r_prefixes_0: "eval r_prefixes [0, j] \<down>= list_encode [j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_prefixes [0, j] \<down>= singleton_encode j
[PROOF STEP]
unfolding r_prefixes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_next) [0, j] \<down>= singleton_encode j
[PROOF STEP]
by simp


[STATEMENT]
lemma deleteMin_correct_aux:
  assumes I: "invar q"
  assumes NE: "q\<noteq>[]"
  shows
  "invar (deleteMin q)"
  "queue_to_multiset_aux (deleteMin q) = queue_to_multiset_aux q -
  {# (findMin q, eprio (findMin q)) #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SkewBinomialHeapStruc.invar (map bsmapt (deleteMin q)) &&& SkewBinomialHeapStruc.queue_to_multiset (map bsmapt (deleteMin q)) = SkewBinomialHeapStruc.queue_to_multiset (map bsmapt q) - {#(findMin q, eprio (findMin q))#}
[PROOF STEP]
apply (simp_all add:
    I NE deleteMin_xlate findMin_xlate_aux
    SkewBinomialHeapStruc.deleteMin_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done