[STATEMENT]
lemma length_neq_imp_not_list_all2:
  assumes "length xs \<noteq> length ys"
  shows "\<not> list_all2 R xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> list_all2 R xs ys
[PROOF STEP]
proof (rule notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_all2 R xs ys \<Longrightarrow> False
[PROOF STEP]
assume "list_all2 R xs ys"
[PROOF STATE]
proof (state)
this:
list_all2 R xs ys

goal (1 subgoal):
 1. list_all2 R xs ys \<Longrightarrow> False
[PROOF STEP]
hence "length xs = length ys"
[PROOF STATE]
proof (prove)
using this:
list_all2 R xs ys

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

goal (1 subgoal):
 1. list_all2 R xs ys \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
length xs = length ys

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
length xs \<noteq> length ys

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_all2_rel_prod_conv:
  "list_all2 (rel_prod R S) xs ys \<longleftrightarrow>
    list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
proof (cases "length xs = length ys")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs = length ys \<Longrightarrow> list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
 2. length xs \<noteq> length ys \<Longrightarrow> list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs = length ys

goal (2 subgoals):
 1. length xs = length ys \<Longrightarrow> list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
 2. length xs \<noteq> length ys \<Longrightarrow> list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs = length ys

goal (1 subgoal):
 1. list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
by (induction xs ys rule: list_induct2) (auto simp: rel_prod_sel)
[PROOF STATE]
proof (state)
this:
list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))

goal (1 subgoal):
 1. length xs \<noteq> length ys \<Longrightarrow> list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length xs \<noteq> length ys \<Longrightarrow> list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length xs \<noteq> length ys

goal (1 subgoal):
 1. length xs \<noteq> length ys \<Longrightarrow> list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
hence neq_length_maps:
      "length (map fst xs) \<noteq> length (map fst ys)"
      "length (map snd xs) \<noteq> length (map snd ys)"
[PROOF STATE]
proof (prove)
using this:
length xs \<noteq> length ys

goal (1 subgoal):
 1. length (map fst xs) \<noteq> length (map fst ys) &&& length (map snd xs) \<noteq> length (map snd ys)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
length (map fst xs) \<noteq> length (map fst ys)
length (map snd xs) \<noteq> length (map snd ys)

goal (1 subgoal):
 1. length xs \<noteq> length ys \<Longrightarrow> list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
using length_neq_imp_not_list_all2[OF False]
[PROOF STATE]
proof (prove)
using this:
\<not> list_all2 ?R xs ys

goal (1 subgoal):
 1. list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
using neq_length_maps[THEN length_neq_imp_not_list_all2]
[PROOF STATE]
proof (prove)
using this:
\<not> list_all2 ?R xs ys
\<not> list_all2 ?R (map fst xs) (map fst ys)
\<not> list_all2 ?R (map snd xs) (map snd ys)

goal (1 subgoal):
 1. list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all2 (rel_prod R S) xs ys = (list_all2 R (map fst xs) (map fst ys) \<and> list_all2 S (map snd xs) (map snd ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rewrite_fundef_body_cases[case_names invalid_label valid_label]:
  assumes
    "\<And>bs ar ret locals. fd = Fundef bs ar ret locals \<Longrightarrow> map_of bs l = None \<Longrightarrow> P"
    "\<And>bs ar ret locals instrs. fd = Fundef bs ar ret locals \<Longrightarrow> map_of bs l = Some instrs \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fd = Fundef ?bs ?ar ?ret ?locals; map_of ?bs l = None\<rbrakk> \<Longrightarrow> P
\<lbrakk>fd = Fundef ?bs ?ar ?ret ?locals; map_of ?bs l = Some ?instrs\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (cases fd; cases "map_of (body fd) l") auto


[STATEMENT]
lemma arity_rewrite_fundef_body[simp]: "arity (rewrite_fundef_body fd l pc instr) = arity fd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arity (rewrite_fundef_body fd l pc instr) = arity fd
[PROOF STEP]
by (cases fd; simp add: rewrite_fundef_body_def option.case_eq_if)


[STATEMENT]
lemma return_rewrite_fundef_body[simp]: "return (rewrite_fundef_body fd l pc instr) = return fd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. return (rewrite_fundef_body fd l pc instr) = return fd
[PROOF STEP]
by (cases fd) (simp add: rewrite_fundef_body_def option.case_eq_if)


[STATEMENT]
lemma funtype_rewrite_fundef_body[simp]: "funtype (rewrite_fundef_body fd l pc instr') = funtype fd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funtype (rewrite_fundef_body fd l pc instr') = funtype fd
[PROOF STEP]
by (simp add: funtype_def)


[STATEMENT]
lemma length_body_rewrite_fundef_body[simp]:
  "length (body (rewrite_fundef_body fd l pc instr)) = length (body fd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (body (rewrite_fundef_body fd l pc instr)) = length (body fd)
[PROOF STEP]
by (cases fd) (simp add: rewrite_fundef_body_def)


[STATEMENT]
lemma prod_in_set_fst_image_conv: "(x, y) \<in> set xys \<Longrightarrow> x \<in> fst ` set xys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> set xys \<Longrightarrow> x \<in> fst ` set xys
[PROOF STEP]
by (metis fstI image_eqI)


[STATEMENT]
lemma map_of_body_rewrite_fundef_body_conv_neq[simp]:
  assumes "l \<noteq> l'"
  shows "map_of (body (rewrite_fundef_body fd l pc instr)) l' = map_of (body fd) l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (body (rewrite_fundef_body fd l pc instr)) l' = map_of (body fd) l'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l \<noteq> l'

goal (1 subgoal):
 1. map_of (body (rewrite_fundef_body fd l pc instr)) l' = map_of (body fd) l'
[PROOF STEP]
by (cases fd) (simp add: rewrite_fundef_body_def map_of_map_entry)


[STATEMENT]
lemma map_of_body_rewrite_fundef_body_conv_eq[simp]:
  "map_of (body (rewrite_fundef_body fd l pc instr)) l =
   map_option (\<lambda>xs. xs[pc := instr]) (map_of (body fd) l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (body (rewrite_fundef_body fd l pc instr)) l = map_option (\<lambda>xs. xs[pc := instr]) (map_of (body fd) l)
[PROOF STEP]
by (cases fd) (simp add: rewrite_fundef_body_def map_of_map_entry map_option_case)


[STATEMENT]
lemma instr_at_rewrite_fundef_body_conv:
  "instr_at (rewrite_fundef_body fd l' pc' instr') l pc =
    map_option (\<lambda>instr. if l = l' \<and> pc = pc' then instr' else instr) (instr_at fd l pc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
proof (cases fd)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. fd = Fundef x1 x2 x3 x4 \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
case (Fundef bblocks ar ret locals)
[PROOF STATE]
proof (state)
this:
fd = Fundef bblocks ar ret locals

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. fd = Fundef x1 x2 x3 x4 \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fd = Fundef bblocks ar ret locals
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fd = Fundef bblocks ar ret locals

goal (1 subgoal):
 1. instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
proof (cases "instr_at fd l pc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>fd = Fundef bblocks ar ret locals; instr_at fd l pc = None\<rbrakk> \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
 2. \<And>a. \<lbrakk>fd = Fundef bblocks ar ret locals; instr_at fd l pc = Some a\<rbrakk> \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
instr_at fd l pc = None

goal (2 subgoals):
 1. \<lbrakk>fd = Fundef bblocks ar ret locals; instr_at fd l pc = None\<rbrakk> \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
 2. \<And>a. \<lbrakk>fd = Fundef bblocks ar ret locals; instr_at fd l pc = Some a\<rbrakk> \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
instr_at fd l pc = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
instr_at fd l pc = None

goal (1 subgoal):
 1. instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
by (cases "map_of bblocks l")
        (auto simp add: Fundef rewrite_fundef_body_def instr_at_def map_of_map_entry)
[PROOF STATE]
proof (state)
this:
instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>fd = Fundef bblocks ar ret locals; instr_at fd l pc = Some a\<rbrakk> \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>fd = Fundef bblocks ar ret locals; instr_at fd l pc = Some a\<rbrakk> \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
case (Some instrs)
[PROOF STATE]
proof (state)
this:
instr_at fd l pc = Some instrs

goal (1 subgoal):
 1. \<And>a. \<lbrakk>fd = Fundef bblocks ar ret locals; instr_at fd l pc = Some a\<rbrakk> \<Longrightarrow> instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
instr_at fd l pc = Some instrs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
instr_at fd l pc = Some instrs

goal (1 subgoal):
 1. instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)
[PROOF STEP]
by (cases "map_of bblocks l")
        (auto simp add: Fundef rewrite_fundef_body_def instr_at_def map_of_map_entry)
[PROOF STATE]
proof (state)
this:
instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
instr_at (rewrite_fundef_body fd l' pc' instr') l pc = map_option (If (l = l' \<and> pc = pc') instr') (instr_at fd l pc)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fundef_locals_rewrite_fundef_body[simp]:
  "fundef_locals (rewrite_fundef_body fd l pc instr) = fundef_locals fd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fundef_locals (rewrite_fundef_body fd l pc instr) = fundef_locals fd
[PROOF STEP]
by (cases fd; simp add: rewrite_fundef_body_def option.case_eq_if)


[STATEMENT]
lemma rel_fundef_rewrite_body1:
  assumes
    rel_fd1_fd2: "rel_fundef (=) R fd1 fd2" and
    instr_at_l_pc: "instr_at fd1 l pc = Some instr" and
    R_iff: "\<And>x. R instr x \<longleftrightarrow> R instr' x"
  shows "rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) R fd1 fd2

goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
proof (cases rule: fundef.rel_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
case (Fundef xs ar' ret' locals' ys ar ret locals)
[PROOF STATE]
proof (state)
this:
fd1 = Fundef xs ar' ret' locals'
fd2 = Fundef ys ar ret locals
list_all2 (rel_prod (=) (list_all2 R)) xs ys
ar' = ar
ret' = ret
locals' = locals

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
using Fundef(3,3,1,2,4-) instr_at_l_pc
[PROOF STATE]
proof (prove)
using this:
list_all2 (rel_prod (=) (list_all2 R)) xs ys
list_all2 (rel_prod (=) (list_all2 R)) xs ys
fd1 = Fundef xs ar' ret' locals'
fd2 = Fundef ys ar ret locals
ar' = ar
ret' = ret
locals' = locals
instr_at fd1 l pc = Some instr

goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
proof (induction xs ys arbitrary: fd1 fd2 rule: list.rel_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fd1 fd2. \<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) [] []; fd1 = Fundef [] ar' ret' locals'; fd2 = Fundef [] ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
 2. \<And>a21 a22 b21 b22 fd1 fd2. \<lbrakk>rel_prod (=) (list_all2 R) a21 b21; \<And>fd1 fd2. \<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) a22 b22; fd1 = Fundef a22 ar' ret' locals'; fd2 = Fundef b22 ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2; list_all2 (rel_prod (=) (list_all2 R)) (a21 # a22) (b21 # b22); fd1 = Fundef (a21 # a22) ar' ret' locals'; fd2 = Fundef (b21 # b22) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
list_all2 (rel_prod (=) (list_all2 R)) [] []
fd1 = Fundef [] ar' ret' locals'
fd2 = Fundef [] ar ret locals
ar' = ar
ret' = ret
locals' = locals
instr_at fd1 l pc = Some instr

goal (2 subgoals):
 1. \<And>fd1 fd2. \<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) [] []; fd1 = Fundef [] ar' ret' locals'; fd2 = Fundef [] ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
 2. \<And>a21 a22 b21 b22 fd1 fd2. \<lbrakk>rel_prod (=) (list_all2 R) a21 b21; \<And>fd1 fd2. \<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) a22 b22; fd1 = Fundef a22 ar' ret' locals'; fd2 = Fundef b22 ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2; list_all2 (rel_prod (=) (list_all2 R)) (a21 # a22) (b21 # b22); fd1 = Fundef (a21 # a22) ar' ret' locals'; fd2 = Fundef (b21 # b22) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all2 (rel_prod (=) (list_all2 R)) [] []
fd1 = Fundef [] ar' ret' locals'
fd2 = Fundef [] ar ret locals
ar' = ar
ret' = ret
locals' = locals
instr_at fd1 l pc = Some instr
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list_all2 (rel_prod (=) (list_all2 R)) [] []
fd1 = Fundef [] ar' ret' locals'
fd2 = Fundef [] ar ret locals
ar' = ar
ret' = ret
locals' = locals
instr_at fd1 l pc = Some instr

goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
by (simp add: rewrite_fundef_body_def)
[PROOF STATE]
proof (state)
this:
rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2

goal (1 subgoal):
 1. \<And>a21 a22 b21 b22 fd1 fd2. \<lbrakk>rel_prod (=) (list_all2 R) a21 b21; \<And>fd1 fd2. \<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) a22 b22; fd1 = Fundef a22 ar' ret' locals'; fd2 = Fundef b22 ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2; list_all2 (rel_prod (=) (list_all2 R)) (a21 # a22) (b21 # b22); fd1 = Fundef (a21 # a22) ar' ret' locals'; fd2 = Fundef (b21 # b22) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a21 a22 b21 b22 fd1 fd2. \<lbrakk>rel_prod (=) (list_all2 R) a21 b21; \<And>fd1 fd2. \<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) a22 b22; fd1 = Fundef a22 ar' ret' locals'; fd2 = Fundef b22 ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2; list_all2 (rel_prod (=) (list_all2 R)) (a21 # a22) (b21 # b22); fd1 = Fundef (a21 # a22) ar' ret' locals'; fd2 = Fundef (b21 # b22) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
case (Cons x xs y ys)
[PROOF STATE]
proof (state)
this:
rel_prod (=) (list_all2 R) x y
\<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) xs ys; ?fd1.0 = Fundef xs ar' ret' locals'; ?fd2.0 = Fundef ys ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at ?fd1.0 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body ?fd1.0 l pc instr') ?fd2.0
list_all2 (rel_prod (=) (list_all2 R)) (x # xs) (y # ys)
fd1 = Fundef (x # xs) ar' ret' locals'
fd2 = Fundef (y # ys) ar ret locals
ar' = ar
ret' = ret
locals' = locals
instr_at fd1 l pc = Some instr

goal (1 subgoal):
 1. \<And>a21 a22 b21 b22 fd1 fd2. \<lbrakk>rel_prod (=) (list_all2 R) a21 b21; \<And>fd1 fd2. \<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) a22 b22; fd1 = Fundef a22 ar' ret' locals'; fd2 = Fundef b22 ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2; list_all2 (rel_prod (=) (list_all2 R)) (a21 # a22) (b21 # b22); fd1 = Fundef (a21 # a22) ar' ret' locals'; fd2 = Fundef (b21 # b22) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at fd1 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rel_prod (=) (list_all2 R) x y
\<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) xs ys; ?fd1.0 = Fundef xs ar' ret' locals'; ?fd2.0 = Fundef ys ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at ?fd1.0 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body ?fd1.0 l pc instr') ?fd2.0
list_all2 (rel_prod (=) (list_all2 R)) (x # xs) (y # ys)
fd1 = Fundef (x # xs) ar' ret' locals'
fd2 = Fundef (y # ys) ar ret locals
ar' = ar
ret' = ret
locals' = locals
instr_at fd1 l pc = Some instr
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rel_prod (=) (list_all2 R) x y
\<lbrakk>list_all2 (rel_prod (=) (list_all2 R)) xs ys; ?fd1.0 = Fundef xs ar' ret' locals'; ?fd2.0 = Fundef ys ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at ?fd1.0 l pc = Some instr\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body ?fd1.0 l pc instr') ?fd2.0
list_all2 (rel_prod (=) (list_all2 R)) (x # xs) (y # ys)
fd1 = Fundef (x # xs) ar' ret' locals'
fd2 = Fundef (y # ys) ar ret locals
ar' = ar
ret' = ret
locals' = locals
instr_at fd1 l pc = Some instr

goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2
[PROOF STEP]
apply (simp add: rewrite_fundef_body_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_prod (=) (list_all2 R) x y; \<And>fd1 fd2. \<lbrakk>fd1 = Fundef xs ar ret locals; fd2 = Fundef ys ar ret locals; instr_at (Fundef xs ar ret locals) l pc = Some instr\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry l (\<lambda>instrs. instrs[pc := instr']) xs) ys; list_all2 (rel_prod (=) (list_all2 R)) xs ys; fd1 = Fundef (x # xs) ar ret locals; fd2 = Fundef (y # ys) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at (Fundef (x # xs) ar ret locals) l pc = Some instr\<rbrakk> \<Longrightarrow> (fst x = l \<longrightarrow> rel_prod (=) (list_all2 R) (l, (snd x)[pc := instr']) y) \<and> (fst x \<noteq> l \<longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry l (\<lambda>instrs. instrs[pc := instr']) xs) ys)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rel_prod (=) (list_all2 R) x y; \<And>fd1 fd2. \<lbrakk>fd1 = Fundef xs ar ret locals; fd2 = Fundef ys ar ret locals; instr_at (Fundef xs ar ret locals) (fst x) pc = Some instr\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry (fst x) (\<lambda>instrs. instrs[pc := instr']) xs) ys; list_all2 (rel_prod (=) (list_all2 R)) xs ys; fd1 = Fundef (x # xs) ar ret locals; fd2 = Fundef (y # ys) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at (Fundef (x # xs) ar ret locals) (fst x) pc = Some instr; l = fst x\<rbrakk> \<Longrightarrow> rel_prod (=) (list_all2 R) (fst x, (snd x)[pc := instr']) y
 2. \<lbrakk>rel_prod (=) (list_all2 R) x y; \<And>fd1 fd2. \<lbrakk>fd1 = Fundef xs ar ret locals; fd2 = Fundef ys ar ret locals; instr_at (Fundef xs ar ret locals) l pc = Some instr\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry l (\<lambda>instrs. instrs[pc := instr']) xs) ys; list_all2 (rel_prod (=) (list_all2 R)) xs ys; fd1 = Fundef (x # xs) ar ret locals; fd2 = Fundef (y # ys) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at (Fundef (x # xs) ar ret locals) l pc = Some instr; fst x \<noteq> l\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry l (\<lambda>instrs. instrs[pc := instr']) xs) ys
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
R instr ?x = R instr' ?x

goal (2 subgoals):
 1. \<lbrakk>rel_prod (=) (list_all2 R) x y; \<And>fd1 fd2. \<lbrakk>fd1 = Fundef xs ar ret locals; fd2 = Fundef ys ar ret locals; instr_at (Fundef xs ar ret locals) (fst x) pc = Some instr\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry (fst x) (\<lambda>instrs. instrs[pc := instr']) xs) ys; list_all2 (rel_prod (=) (list_all2 R)) xs ys; fd1 = Fundef (x # xs) ar ret locals; fd2 = Fundef (y # ys) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at (Fundef (x # xs) ar ret locals) (fst x) pc = Some instr; l = fst x\<rbrakk> \<Longrightarrow> rel_prod (=) (list_all2 R) (fst x, (snd x)[pc := instr']) y
 2. \<lbrakk>rel_prod (=) (list_all2 R) x y; \<And>fd1 fd2. \<lbrakk>fd1 = Fundef xs ar ret locals; fd2 = Fundef ys ar ret locals; instr_at (Fundef xs ar ret locals) l pc = Some instr\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry l (\<lambda>instrs. instrs[pc := instr']) xs) ys; list_all2 (rel_prod (=) (list_all2 R)) xs ys; fd1 = Fundef (x # xs) ar ret locals; fd2 = Fundef (y # ys) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at (Fundef (x # xs) ar ret locals) l pc = Some instr; fst x \<noteq> l\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry l (\<lambda>instrs. instrs[pc := instr']) xs) ys
[PROOF STEP]
apply (smt (verit, ccfv_SIG) fun_upd_apply fundef.sel(1) instr_atD list_all2_lengthD
          list_all2_nthD2 list_all2_update1_cong map_of.simps(2) option.simps(1) prod.sel(1,2)
          rel_prod_sel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_prod (=) (list_all2 R) x y; \<And>fd1 fd2. \<lbrakk>fd1 = Fundef xs ar ret locals; fd2 = Fundef ys ar ret locals; instr_at (Fundef xs ar ret locals) l pc = Some instr\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry l (\<lambda>instrs. instrs[pc := instr']) xs) ys; list_all2 (rel_prod (=) (list_all2 R)) xs ys; fd1 = Fundef (x # xs) ar ret locals; fd2 = Fundef (y # ys) ar ret locals; ar' = ar; ret' = ret; locals' = locals; instr_at (Fundef (x # xs) ar ret locals) l pc = Some instr; fst x \<noteq> l\<rbrakk> \<Longrightarrow> list_all2 (rel_prod (=) (list_all2 R)) (AList.map_entry l (\<lambda>instrs. instrs[pc := instr']) xs) ys
[PROOF STEP]
by (simp add: instr_at_def)
[PROOF STATE]
proof (state)
this:
rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_fundef (=) R (rewrite_fundef_body fd1 l pc instr') fd2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_fundef_rewrite_body:
  assumes rel_fd1_fd2: "rel_fundef (=) R fd1 fd2" and R_i1_i2: "R i1 i2"
  shows "rel_fundef (=) R (rewrite_fundef_body fd1 l pc i1) (rewrite_fundef_body fd2 l pc i2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc i1) (rewrite_fundef_body fd2 l pc i2)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) R fd1 fd2

goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc i1) (rewrite_fundef_body fd2 l pc i2)
[PROOF STEP]
proof (cases rule: fundef.rel_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc i1) (rewrite_fundef_body fd2 l pc i2)
[PROOF STEP]
case (Fundef bblocks1 ar1 ret1 locals1 bblocks2 ar2 ret2 locals2)
[PROOF STATE]
proof (state)
this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R (rewrite_fundef_body fd1 l pc i1) (rewrite_fundef_body fd2 l pc i2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2

goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc i1) (rewrite_fundef_body fd2 l pc i2)
[PROOF STEP]
using R_i1_i2
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2
R i1 i2

goal (1 subgoal):
 1. rel_fundef (=) R (rewrite_fundef_body fd1 l pc i1) (rewrite_fundef_body fd2 l pc i2)
[PROOF STEP]
by (auto simp: rewrite_fundef_body_def
      intro!: list_all2_update_cong
      intro!: list_all2_rel_prod_map_entry
      dest: rel_option_map_of[of _ _ _ l])
[PROOF STATE]
proof (state)
this:
rel_fundef (=) R (rewrite_fundef_body fd1 l pc i1) (rewrite_fundef_body fd2 l pc i2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rewrite_fundef_body_triv:
  "instr_at fd l pc = Some instr \<Longrightarrow> rewrite_fundef_body fd l pc instr = fd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instr_at fd l pc = Some instr \<Longrightarrow> rewrite_fundef_body fd l pc instr = fd
[PROOF STEP]
by (cases fd)
    (auto simp add: rewrite_fundef_body_def map_entry_map_of_Some_conv update_triv dest: instr_atD)


[STATEMENT]
lemma rel_fundef_rewrite_body2:
  assumes
    rel_fd1_fd2: "rel_fundef (=) R fd1 fd2" and
    instr_at_l_pc: "instr_at fd2 l pc = Some instr" and
    R_iff: "\<And>x. R x instr \<longleftrightarrow> R x instr'"
  shows "rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) R fd1 fd2

goal (1 subgoal):
 1. rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
proof (cases rule: fundef.rel_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
case (Fundef xs ar' ret' locals' ys ar ret locals)
[PROOF STATE]
proof (state)
this:
fd1 = Fundef xs ar' ret' locals'
fd2 = Fundef ys ar ret locals
list_all2 (rel_prod (=) (list_all2 R)) xs ys
ar' = ar
ret' = ret
locals' = locals

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fd1 = Fundef xs ar' ret' locals'
fd2 = Fundef ys ar ret locals
list_all2 (rel_prod (=) (list_all2 R)) xs ys
ar' = ar
ret' = ret
locals' = locals

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
obtain instrs2 where
    "map_of (body fd2) l = Some instrs2" and "pc < length instrs2" and "instrs2 ! pc = instr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>instrs2. \<lbrakk>map_of (body fd2) l = Some instrs2; pc < length instrs2; instrs2 ! pc = instr\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using instr_atD[OF instr_at_l_pc]
[PROOF STATE]
proof (prove)
using this:
\<exists>instrs. map_of (body fd2) l = Some instrs \<and> pc < length instrs \<and> instrs ! pc = instr

goal (1 subgoal):
 1. (\<And>instrs2. \<lbrakk>map_of (body fd2) l = Some instrs2; pc < length instrs2; instrs2 ! pc = instr\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr
[PROOF STEP]
obtain instrs1 instr1 where
    "map_of (body fd1) l = Some instrs1" and "pc < length instrs1" and "instrs1 ! pc = instr1"
[PROOF STATE]
proof (prove)
using this:
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr

goal (1 subgoal):
 1. (\<And>instrs1 instr1. \<lbrakk>map_of (body fd1) l = Some instrs1; pc < length instrs1; instrs1 ! pc = instr1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rel_fundef_imp_rel_option_instr_at[OF rel_fd1_fd2, of l pc]
[PROOF STATE]
proof (prove)
using this:
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr
rel_option R (instr_at fd1 l pc) (instr_at fd2 l pc)

goal (1 subgoal):
 1. (\<And>instrs1 instr1. \<lbrakk>map_of (body fd1) l = Some instrs1; pc < length instrs1; instrs1 ! pc = instr1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp add: instr_at_def option_rel_Some2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x'. \<lbrakk>\<And>instrs1 instr1. \<lbrakk>map_of (body fd1) l = Some instrs1; pc < length instrs1; instrs1 ! pc = instr1\<rbrakk> \<Longrightarrow> thesis; map_of (body fd2) l = Some instrs2; pc < length instrs2; instr = instrs2 ! pc; (case map_of (body fd1) l of None \<Rightarrow> None | Some instrs \<Rightarrow> if pc < length instrs then Some (instrs ! pc) else None) = Some x'; R x' (instrs2 ! pc)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis instr_atD instr_at_def)
[PROOF STATE]
proof (state)
this:
map_of (body fd1) l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of (body fd1) l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
have "list_all2 R instrs1 instrs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 R instrs1 instrs2
[PROOF STEP]
using Fundef \<open>map_of (body fd2) l = Some instrs2\<close> \<open>map_of (body fd1) l = Some instrs1\<close>
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef xs ar' ret' locals'
fd2 = Fundef ys ar ret locals
list_all2 (rel_prod (=) (list_all2 R)) xs ys
ar' = ar
ret' = ret
locals' = locals
map_of (body fd2) l = Some instrs2
map_of (body fd1) l = Some instrs1

goal (1 subgoal):
 1. list_all2 R instrs1 instrs2
[PROOF STEP]
by (auto dest: rel_option_map_of[of _ _ _ l])
[PROOF STATE]
proof (state)
this:
list_all2 R instrs1 instrs2

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all2 R instrs1 instrs2

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
hence "R (instrs1 ! pc) (instrs2 ! pc)"
[PROOF STATE]
proof (prove)
using this:
list_all2 R instrs1 instrs2

goal (1 subgoal):
 1. R (instrs1 ! pc) (instrs2 ! pc)
[PROOF STEP]
using \<open>pc < length instrs1\<close>
[PROOF STATE]
proof (prove)
using this:
list_all2 R instrs1 instrs2
pc < length instrs1

goal (1 subgoal):
 1. R (instrs1 ! pc) (instrs2 ! pc)
[PROOF STEP]
by (auto intro: list_all2_nthD)
[PROOF STATE]
proof (state)
this:
R (instrs1 ! pc) (instrs2 ! pc)

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fd1 = Fundef xs ar' ret' locals'
fd2 = Fundef ys ar ret locals
list_all2 (rel_prod (=) (list_all2 R)) xs ys
ar' = ar
ret' = ret
locals' = locals
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr
map_of (body fd1) l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1
list_all2 R instrs1 instrs2
R (instrs1 ! pc) (instrs2 ! pc)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef xs ar' ret' locals'
fd2 = Fundef ys ar ret locals
list_all2 (rel_prod (=) (list_all2 R)) xs ys
ar' = ar
ret' = ret
locals' = locals
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr
map_of (body fd1) l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1
list_all2 R instrs1 instrs2
R (instrs1 ! pc) (instrs2 ! pc)

goal (1 subgoal):
 1. rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')
[PROOF STEP]
by (auto simp: rewrite_fundef_body_def R_iff
          intro!: list_all2_rel_prod_map_entry2
          intro: list_all2_update2_cong)
[PROOF STATE]
proof (state)
this:
rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_fundef_rewrite_body2':
  assumes
    rel_fd1_fd2: "rel_fundef (=) R fd1 fd2" and
    instr_at1: "instr_at fd1 l pc = Some instr1" and
    R_instr1_instr2: "R instr1 instr2'"
  shows "rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) R fd1 fd2

goal (1 subgoal):
 1. rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
proof (cases rule: fundef.rel_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
case (Fundef bblocks1 ar1 ret1 locals1 bblocks2 ar2 ret2 locals2)
[PROOF STATE]
proof (state)
this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
obtain instrs1 where
    "map_of bblocks1 l = Some instrs1" and "pc < length instrs1" and "instrs1 ! pc = instr1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>instrs1. \<lbrakk>map_of bblocks1 l = Some instrs1; pc < length instrs1; instrs1 ! pc = instr1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Fundef instr_at1[THEN instr_atD]
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2
\<exists>instrs. map_of (body fd1) l = Some instrs \<and> pc < length instrs \<and> instrs ! pc = instr1

goal (1 subgoal):
 1. (\<And>instrs1. \<lbrakk>map_of bblocks1 l = Some instrs1; pc < length instrs1; instrs1 ! pc = instr1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_of bblocks1 l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
map_of bblocks1 l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map_of bblocks1 l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1
[PROOF STEP]
obtain instrs2 instr2 where
    "map_of (body fd2) l = Some instrs2" and "pc < length instrs2" and "instrs2 ! pc = instr2"
[PROOF STATE]
proof (prove)
using this:
map_of bblocks1 l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1

goal (1 subgoal):
 1. (\<And>instrs2 instr2. \<lbrakk>map_of (body fd2) l = Some instrs2; pc < length instrs2; instrs2 ! pc = instr2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Fundef rel_fd1_fd2
[PROOF STATE]
proof (prove)
using this:
map_of bblocks1 l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2
rel_fundef (=) R fd1 fd2

goal (1 subgoal):
 1. (\<And>instrs2 instr2. \<lbrakk>map_of (body fd2) l = Some instrs2; pc < length instrs2; instrs2 ! pc = instr2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (auto simp: option_rel_Some1 dest!: rel_option_map_of[where l = l])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>\<And>instrs2 instr2. \<lbrakk>y' = instrs2; pc < length instrs2; instrs2 ! pc = instr2\<rbrakk> \<Longrightarrow> thesis; map_of bblocks1 l = Some instrs1; pc < length instrs1; fd1 = Fundef bblocks1 ar2 ret2 locals2; fd2 = Fundef bblocks2 ar2 ret2 locals2; ar1 = ar2; ret1 = ret2; locals1 = locals2; instr1 = instrs1 ! pc; map_of bblocks2 l = Some y'; list_all2 R instrs1 y'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr2

goal (1 subgoal):
 1. \<And>x1a x2a x3a x4a y1a y2a y3a y4a. \<lbrakk>fd1 = Fundef x1a x2a x3a x4a; fd2 = Fundef y1a y2a y3a y4a; list_all2 (rel_prod (=) (list_all2 R)) x1a y1a; x2a = y2a; x3a = y3a; x4a = y4a\<rbrakk> \<Longrightarrow> rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2
map_of bblocks1 l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2
map_of bblocks1 l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr2

goal (1 subgoal):
 1. rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
using R_instr1_instr2
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef bblocks1 ar1 ret1 locals1
fd2 = Fundef bblocks2 ar2 ret2 locals2
list_all2 (rel_prod (=) (list_all2 R)) bblocks1 bblocks2
ar1 = ar2
ret1 = ret2
locals1 = locals2
map_of bblocks1 l = Some instrs1
pc < length instrs1
instrs1 ! pc = instr1
map_of (body fd2) l = Some instrs2
pc < length instrs2
instrs2 ! pc = instr2
R instr1 instr2'

goal (1 subgoal):
 1. rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')
[PROOF STEP]
by (auto simp: rewrite_fundef_body_def
          intro!: list_all2_update2_cong list_all2_rel_prod_map_entry2
          dest: rel_option_map_of[of _ _ _ l])
[PROOF STATE]
proof (state)
this:
rel_fundef (=) R fd1 (rewrite_fundef_body fd2 l pc instr2')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma if_eq_const_conv: "(if x then y else z) = w \<longleftrightarrow> x \<and> y = w \<or> \<not> x \<and> z = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if x then y else z) = w) = (x \<and> y = w \<or> \<not> x \<and> z = w)
[PROOF STEP]
by simp


[STATEMENT]
lemma const_eq_if_conv: "w = (if x then y else z) \<longleftrightarrow> x \<and> w = y \<or> \<not> x \<and> w = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w = (if x then y else z)) = (x \<and> w = y \<or> \<not> x \<and> w = z)
[PROOF STEP]
by auto


[STATEMENT]
lemma pure_vec_nth [simp]: "pure_vec x $ i = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure_vec x $ i = x
[PROOF STEP]
by(simp add: pure_vec_def)


[STATEMENT]
lemma ap_vec_nth [simp]: "ap_vec f x $ i  = (f $ i) (x $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Applicative.ap f x $ i = (f $ i) (x $ i)
[PROOF STEP]
by(simp add: ap_vec_def)


[STATEMENT]
lemma stake_run:
      assumes "\<And> k. path (stake k r) p"
      shows "run r p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run r p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path (stake ?k r) p

goal (1 subgoal):
 1. run r p
[PROOF STEP]
by (coinduction arbitrary: r p) (force elim: path.cases)


[STATEMENT]
lemma snth_run:
      assumes "\<And> k. enabled (r !! k) (target (stake k r) p)"
      shows "run r p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run r p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
enabled (r !! ?k) (target (stake ?k r) p)

goal (1 subgoal):
 1. run r p
[PROOF STEP]
by (coinduction arbitrary: r p) (metis stream.sel fold_simps snth.simps stake.simps)


[STATEMENT]
lemma run_stake:
      assumes "run r p"
      shows "path (stake k r) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (stake k r) p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run r p

goal (1 subgoal):
 1. path (stake k r) p
[PROOF STEP]
by (metis run_shift_elim stake_sdrop)


[STATEMENT]
lemma run_sdrop:
      assumes "run r p"
      shows "run (sdrop k r) (target (stake k r) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run (sdrop k r) (target (stake k r) p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run r p

goal (1 subgoal):
 1. run (sdrop k r) (target (stake k r) p)
[PROOF STEP]
by (metis run_shift_elim stake_sdrop)


[STATEMENT]
lemma run_snth:
      assumes "run r p"
      shows "enabled (r !! k) (target (stake k r) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enabled (r !! k) (target (stake k r) p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
run r p

goal (1 subgoal):
 1. enabled (r !! k) (target (stake k r) p)
[PROOF STEP]
by (metis stream.collapse sdrop_simps(1) run_scons_elim run_sdrop)


[STATEMENT]
lemma run_alt_def_snth: "run r p \<longleftrightarrow> (\<forall> k. enabled (r !! k) (target (stake k r) p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run r p = (\<forall>k. enabled (r !! k) (target (stake k r) p))
[PROOF STEP]
using snth_run run_snth
[PROOF STATE]
proof (prove)
using this:
(\<And>k. enabled (?r !! k) (target (stake k ?r) ?p)) \<Longrightarrow> run ?r ?p
run ?r ?p \<Longrightarrow> enabled (?r !! ?k) (target (stake ?k ?r) ?p)

goal (1 subgoal):
 1. run r p = (\<forall>k. enabled (r !! k) (target (stake k r) p))
[PROOF STEP]
by blast


[STATEMENT]
lemma reachable_states:
      assumes "q \<in> reachable p" "path r q"
      shows "set (states r q) \<subseteq> reachable p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (states r q) \<subseteq> reachable p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> reachable p
path r q

goal (1 subgoal):
 1. set (states r q) \<subseteq> reachable p
[PROOF STEP]
by (induct r arbitrary: q) (auto)


[STATEMENT]
lemma nodes_states:
      assumes "p \<in> nodes" "path r p"
      shows "set (states r p) \<subseteq> nodes"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (states r p) \<subseteq> nodes
[PROOF STEP]
using reachable_states assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> reachable ?p; path ?r ?q\<rbrakk> \<Longrightarrow> set (states ?r ?q) \<subseteq> reachable ?p
p \<in> nodes
path r p

goal (1 subgoal):
 1. set (states r p) \<subseteq> nodes
[PROOF STEP]
by blast


[STATEMENT]
lemma nodes_trace:
      assumes "p \<in> nodes" "run r p"
      shows "sset (trace r p) \<subseteq> nodes"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset (trace r p) \<subseteq> nodes
[PROOF STEP]
using reachable_trace assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?q \<in> reachable ?p; run ?r ?q\<rbrakk> \<Longrightarrow> sset (trace ?r ?q) \<subseteq> reachable ?p
p \<in> nodes
run r p

goal (1 subgoal):
 1. sset (trace r p) \<subseteq> nodes
[PROOF STEP]
by blast


[STATEMENT]
lemma vars_example_1 :
  fixes e::"('v,integer) aexp"
  assumes "e = (\<lambda> \<sigma>. \<sigma> x - \<sigma> y)"
  assumes "x \<noteq> y"
  shows   "vars e = {x,y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars e = {x, y}
[PROOF STEP]
unfolding set_eq_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xa. (xa \<in> vars e) = (xa \<in> {x, y})
[PROOF STEP]
proof (intro allI iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> vars e \<Longrightarrow> xa \<in> {x, y}
 2. \<And>xa. xa \<in> {x, y} \<Longrightarrow> xa \<in> vars e
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> vars e \<Longrightarrow> xa \<in> {x, y}
 2. \<And>xa. xa \<in> {x, y} \<Longrightarrow> xa \<in> vars e
[PROOF STEP]
assume "v \<in> vars e"
[PROOF STATE]
proof (state)
this:
v \<in> vars e

goal (2 subgoals):
 1. \<And>xa. xa \<in> vars e \<Longrightarrow> xa \<in> {x, y}
 2. \<And>xa. xa \<in> {x, y} \<Longrightarrow> xa \<in> vars e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> vars e
[PROOF STEP]
obtain \<sigma> val
  where "e (\<sigma>(v := val)) \<noteq> e \<sigma>"
[PROOF STATE]
proof (prove)
using this:
v \<in> vars e

goal (1 subgoal):
 1. (\<And>\<sigma> val. e (\<sigma>(v := val)) \<noteq> e \<sigma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {v. \<exists>\<sigma> val. e (\<sigma>(v := val)) \<noteq> e \<sigma>}

goal (1 subgoal):
 1. (\<And>\<sigma> val. e (\<sigma>(v := val)) \<noteq> e \<sigma> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e (\<sigma>(v := val)) \<noteq> e \<sigma>

goal (2 subgoals):
 1. \<And>xa. xa \<in> vars e \<Longrightarrow> xa \<in> {x, y}
 2. \<And>xa. xa \<in> {x, y} \<Longrightarrow> xa \<in> vars e
[PROOF STEP]
thus "v \<in> {x, y}"
[PROOF STATE]
proof (prove)
using this:
e (\<sigma>(v := val)) \<noteq> e \<sigma>

goal (1 subgoal):
 1. v \<in> {x, y}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
e (\<sigma>(v := val)) \<noteq> e \<sigma>
e = (\<lambda>\<sigma>. \<sigma> x - \<sigma> y)
x \<noteq> y

goal (1 subgoal):
 1. v \<in> {x, y}
[PROOF STEP]
by (case_tac "v = x", simp, (case_tac "v = y", simp+))
[PROOF STATE]
proof (state)
this:
v \<in> {x, y}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {x, y} \<Longrightarrow> xa \<in> vars e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {x, y} \<Longrightarrow> xa \<in> vars e
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> {x, y} \<Longrightarrow> xa \<in> vars e
[PROOF STEP]
assume "v \<in> {x,y}"
[PROOF STATE]
proof (state)
this:
v \<in> {x, y}

goal (1 subgoal):
 1. \<And>xa. xa \<in> {x, y} \<Longrightarrow> xa \<in> vars e
[PROOF STEP]
thus "v \<in> vars e"
[PROOF STATE]
proof (prove)
using this:
v \<in> {x, y}

goal (1 subgoal):
 1. v \<in> vars e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> {x, y}
e = (\<lambda>\<sigma>. \<sigma> x - \<sigma> y)
x \<noteq> y

goal (1 subgoal):
 1. v \<in> vars e
[PROOF STEP]
by (auto simp add : vars_def)
     (rule_tac ?x="\<lambda> v. 0" in exI, rule_tac ?x="1" in exI, simp)+
[PROOF STATE]
proof (state)
this:
v \<in> vars e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vars_example_2 :
  fixes e::"('v,integer) aexp"
  assumes "e = (\<lambda> \<sigma>. \<sigma> x - \<sigma> y)"
  assumes "x = y"
  shows   "vars e = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars e = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
e = (\<lambda>\<sigma>. \<sigma> x - \<sigma> y)
x = y

goal (1 subgoal):
 1. vars e = {}
[PROOF STEP]
by (auto simp add : vars_def)


[STATEMENT]
lemma alpha_dioph[dioph]:
  fixes B N X
  defines "D \<equiv> [X = \<alpha> B N]"
  shows "is_dioph_rel D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define r s t u v w x y where param_defs:
    "r == (Param 0)" "s == (Param 1)" "t == (Param 2)" "u == (Param 3)"  "v == (Param 4)"
    "w == (Param 5)" "x == (Param 6)" "y == (Param 7)"
[PROOF STATE]
proof (state)
this:
r \<equiv> polynomial.Param 0
s \<equiv> polynomial.Param 1
t \<equiv> polynomial.Param 2
u \<equiv> polynomial.Param 3
v \<equiv> polynomial.Param 4
w \<equiv> polynomial.Param 5
x \<equiv> polynomial.Param 6
y \<equiv> polynomial.Param 7

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define B' X' N' where pushed_defs: "B' ==  (push_param B 8)" "X' ==  (push_param X 8)"
                                      "N' ==  (push_param N 8)"
[PROOF STATE]
proof (state)
this:
B' \<equiv> push_param B 8
X' \<equiv> push_param X 8
N' \<equiv> push_param N 8

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
(* eqns. (3.41) ? (3.55) from YuMat lecture notes (p. 36) where "a" = X and "c" = N here *)
  (* don't confuse capital X with x == (param 6) here, this is unhappy notation *)
[PROOF STATE]
proof (state)
this:
B' \<equiv> push_param B 8
X' \<equiv> push_param X 8
N' \<equiv> push_param N 8

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define DR1 where "DR1 \<equiv> B' [>] (Const 3) [\<and>] (Const 1 [+] B' [*] u [*] t [=] u[^2] [+] t[^2])"
[PROOF STATE]
proof (state)
this:
DR1 \<equiv> B' [>] polynomial.Const 3 [\<and>] polynomial.Const 1 [+] B' [*] u [*] t [=] u [^2] [+] t [^2]

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define DR2 where "DR2 \<equiv> (Const 1 [+] B' [*] s [*] r [=] s[^2] [+] r[^2]) [\<and>] r [<] s"
[PROOF STATE]
proof (state)
this:
DR2 \<equiv> polynomial.Const 1 [+] B' [*] s [*] r [=] s [^2] [+] r [^2] [\<and>] r [<] s

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define DR3 where "DR3 \<equiv> (DVD (u[^2]) s) [\<and>] (v [+] (Const 2) [*] r [=] B' [*] s)"
[PROOF STATE]
proof (state)
this:
DR3 \<equiv> DVD u [^2] s [\<and>] v [+] polynomial.Const 2 [*] r [=] B' [*] s

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define DR4 where "DR4 \<equiv> (MOD B' v w) [\<and>] (MOD (Const 2) u w) [\<and>] (Const 2) [<] w"
[PROOF STATE]
proof (state)
this:
DR4 \<equiv> MOD B' v w [\<and>] MOD polynomial.Const 2 u w [\<and>] polynomial.Const 2 [<] w

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define DR5 where "DR5 \<equiv> (Const 1 [+] w [*] x [*] y [=] x[^2] [+] y[^2])"
[PROOF STATE]
proof (state)
this:
DR5 \<equiv> polynomial.Const 1 [+] w [*] x [*] y [=] x [^2] [+] y [^2]

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define DR6 where "DR6 \<equiv> (Const 2) [*] X' [<] u [\<and>] (Const 2) [*] X' [<] v
                           [\<and>] (MOD x v X') [\<and>] (Const 2) [*] N' [<] u [\<and>] MOD x u N'"
[PROOF STATE]
proof (state)
this:
DR6 \<equiv> polynomial.Const 2 [*] X' [<] u [\<and>] polynomial.Const 2 [*] X' [<] v [\<and>] MOD x v X' [\<and>] polynomial.Const 2 [*] N' [<] u [\<and>] MOD x u N'

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
define DR where "DR \<equiv> [\<exists>8] DR1 [\<and>] DR2 [\<and>] DR3 [\<and>] DR4 [\<and>] DR5 [\<and>] DR6"
[PROOF STATE]
proof (state)
this:
DR \<equiv> [\<exists>8] DR1 [\<and>] DR2 [\<and>] DR3 [\<and>] DR4 [\<and>] DR5 [\<and>] DR6

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
(* definition would otherwise be too long to handle for Isabelle *)
[PROOF STATE]
proof (state)
this:
DR \<equiv> [\<exists>8] DR1 [\<and>] DR2 [\<and>] DR3 [\<and>] DR4 [\<and>] DR5 [\<and>] DR6

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
note DR_defs = DR1_def DR2_def DR3_def DR4_def DR5_def DR6_def
[PROOF STATE]
proof (state)
this:
DR1 \<equiv> B' [>] polynomial.Const 3 [\<and>] polynomial.Const 1 [+] B' [*] u [*] t [=] u [^2] [+] t [^2]
DR2 \<equiv> polynomial.Const 1 [+] B' [*] s [*] r [=] s [^2] [+] r [^2] [\<and>] r [<] s
DR3 \<equiv> DVD u [^2] s [\<and>] v [+] polynomial.Const 2 [*] r [=] B' [*] s
DR4 \<equiv> MOD B' v w [\<and>] MOD polynomial.Const 2 u w [\<and>] polynomial.Const 2 [<] w
DR5 \<equiv> polynomial.Const 1 [+] w [*] x [*] y [=] x [^2] [+] y [^2]
DR6 \<equiv> polynomial.Const 2 [*] X' [<] u [\<and>] polynomial.Const 2 [*] X' [<] v [\<and>] MOD x v X' [\<and>] polynomial.Const 2 [*] N' [<] u [\<and>] MOD x u N'

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
have "is_dioph_rel DR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel DR
[PROOF STEP]
unfolding DR_def DR_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel ([\<exists>8] B' [>] polynomial.Const 3 [\<and>] polynomial.Const 1 [+] B' [*] u [*] t [=] u [^2] [+] t [^2] [\<and>] (polynomial.Const 1 [+] B' [*] s [*] r [=] s [^2] [+] r [^2] [\<and>] r [<] s) [\<and>] (DVD u [^2] s [\<and>] v [+] polynomial.Const 2 [*] r [=] B' [*] s) [\<and>] (MOD B' v w [\<and>] MOD polynomial.Const 2 u w [\<and>] polynomial.Const 2 [<] w) [\<and>] polynomial.Const 1 [+] w [*] x [*] y [=] x [^2] [+] y [^2] [\<and>] (polynomial.Const 2 [*] X' [<] u [\<and>] polynomial.Const 2 [*] X' [<] v [\<and>] MOD x v X' [\<and>] polynomial.Const 2 [*] N' [<] u [\<and>] MOD x u N'))
[PROOF STEP]
by (auto simp: dioph)
[PROOF STATE]
proof (state)
this:
is_dioph_rel DR

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_dioph_rel DR

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
have "eval D a = eval DR a" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval D a = eval DR a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval D a = eval DR a
[PROOF STEP]
define x_ev b n where evaled_defs: "x_ev \<equiv> peval X a" "b \<equiv> peval B a" "n \<equiv> peval N a"
[PROOF STATE]
proof (state)
this:
x_ev \<equiv> peval X a
b \<equiv> peval B a
n \<equiv> peval N a

goal (1 subgoal):
 1. eval D a = eval DR a
[PROOF STEP]
have h: "eval D a = (\<exists>r s t u v w x y::nat. Exp_Matrices.alpha_equations x_ev b n r s t u v w x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval D a = (\<exists>r s t u v w x y. Exp_Matrices.alpha_equations x_ev b n r s t u v w x y)
[PROOF STEP]
unfolding D_def alpha_def evaled_defs defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (NARY (\<lambda>l. 3 < l ! 0 \<and> int (l ! 2) = Exp_Matrices.\<alpha> (l ! 0) (l ! 1)) [B, N, X]) a = (\<exists>r s t u v w x y. Exp_Matrices.alpha_equations (peval X a) (peval B a) (peval N a) r s t u v w x y)
[PROOF STEP]
using alpha_equivalence
[PROOF STATE]
proof (prove)
using this:
(3 < ?b \<and> int ?a = Exp_Matrices.\<alpha> ?b ?c) = (\<exists>r s t u v w x y. Exp_Matrices.alpha_equations ?a ?b ?c r s t u v w x y)

goal (1 subgoal):
 1. eval (NARY (\<lambda>l. 3 < l ! 0 \<and> int (l ! 2) = Exp_Matrices.\<alpha> (l ! 0) (l ! 1)) [B, N, X]) a = (\<exists>r s t u v w x y. Exp_Matrices.alpha_equations (peval X a) (peval B a) (peval N a) r s t u v w x y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval D a = (\<exists>r s t u v w x y. Exp_Matrices.alpha_equations x_ev b n r s t u v w x y)

goal (1 subgoal):
 1. eval D a = eval DR a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval D a = eval DR a
[PROOF STEP]
proof (rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eval D a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval D a
[PROOF STEP]
assume "eval D a"
[PROOF STATE]
proof (state)
this:
eval D a

goal (2 subgoals):
 1. eval D a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval D a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval D a
[PROOF STEP]
obtain r s t u v w x y :: nat where "Exp_Matrices.alpha_equations x_ev b n r s t u v w x y"
[PROOF STATE]
proof (prove)
using this:
eval D a

goal (1 subgoal):
 1. (\<And>r s t u v w x y. Exp_Matrices.alpha_equations x_ev b n r s t u v w x y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
eval D a
eval D a = (\<exists>r s t u v w x y. Exp_Matrices.alpha_equations x_ev b n r s t u v w x y)

goal (1 subgoal):
 1. (\<And>r s t u v w x y. Exp_Matrices.alpha_equations x_ev b n r s t u v w x y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Exp_Matrices.alpha_equations x_ev b n r s t u v w x y

goal (2 subgoals):
 1. eval D a \<Longrightarrow> eval DR a
 2. eval DR a \<Longrightarrow> eval D a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Exp_Matrices.alpha_equations x_ev b n r s t u v w x y
[PROOF STEP]
show "eval DR a"
[PROOF STATE]
proof (prove)
using this:
Exp_Matrices.alpha_equations x_ev b n r s t u v w x y

goal (1 subgoal):
 1. eval DR a
[PROOF STEP]
unfolding evaled_defs Exp_Matrices.alpha_equations_def
[PROOF STATE]
proof (prove)
using this:
3 < peval B a \<and> u\<^sup>2 + t\<^sup>2 = 1 + peval B a * u * t \<and> s\<^sup>2 + r\<^sup>2 = 1 + peval B a * s * r \<and> r < s \<and> u\<^sup>2 dvd s \<and> v + 2 * r = peval B a * s \<and> w mod v = peval B a mod v \<and> w mod u = 2 mod u \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < u \<and> 2 * peval X a < v \<and> peval X a mod v = x mod v \<and> 2 * peval N a < u \<and> peval N a mod u = x mod u

goal (1 subgoal):
 1. eval DR a
[PROOF STEP]
unfolding DR_def DR_defs defs param_defs
[PROOF STATE]
proof (prove)
using this:
3 < peval B a \<and> u\<^sup>2 + t\<^sup>2 = 1 + peval B a * u * t \<and> s\<^sup>2 + r\<^sup>2 = 1 + peval B a * s * r \<and> r < s \<and> u\<^sup>2 dvd s \<and> v + 2 * r = peval B a * s \<and> w mod v = peval B a mod v \<and> w mod u = 2 mod u \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < u \<and> 2 * peval X a < v \<and> peval X a mod v = x mod v \<and> 2 * peval N a < u \<and> peval N a mod u = x mod u

goal (1 subgoal):
 1. eval ([\<exists>8] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 3, B'] [\<and>] NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Const 1 [+] B' [*] polynomial.Param 3 [*] polynomial.Param 2, polynomial.Param 3 [^2] [+] polynomial.Param 2 [^2]] [\<and>] (NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Const 1 [+] B' [*] polynomial.Param 1 [*] polynomial.Param 0, polynomial.Param 1 [^2] [+] polynomial.Param 0 [^2]] [\<and>] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Param 0, polynomial.Param 1]) [\<and>] (NARY (\<lambda>l. l ! 0 dvd l ! 1) [polynomial.Param 3 [^2], polynomial.Param 1] [\<and>] NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Param 4 [+] polynomial.Const 2 [*] polynomial.Param 0, B' [*] polynomial.Param 1]) [\<and>] (NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [B', polynomial.Param 4, polynomial.Param 5] [\<and>] NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [polynomial.Const 2, polynomial.Param 3, polynomial.Param 5] [\<and>] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 2, polynomial.Param 5]) [\<and>] NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Const 1 [+] polynomial.Param 5 [*] polynomial.Param 6 [*] polynomial.Param 7, polynomial.Param 6 [^2] [+] polynomial.Param 7 [^2]] [\<and>] (NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 2 [*] X', polynomial.Param 3] [\<and>] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 2 [*] X', polynomial.Param 4] [\<and>] NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [polynomial.Param 6, polynomial.Param 4, X'] [\<and>] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 2 [*] N', polynomial.Param 3] [\<and>] NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [polynomial.Param 6, polynomial.Param 3, N'])) a
[PROOF STEP]
apply (auto simp: sq_p_eval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 < peval B a; u\<^sup>2 + t\<^sup>2 = Suc (peval B a * u * t); s\<^sup>2 + r\<^sup>2 = Suc (peval B a * s * r); r < s; u\<^sup>2 dvd s; v + 2 * r = peval B a * s; w mod v = peval B a mod v; w mod u = 2 mod u; 2 < w; x\<^sup>2 + y\<^sup>2 = Suc (w * x * y); 2 * (x mod v) < u; 2 * (x mod v) < v; peval X a = x mod v; 2 * (x mod u) < u; peval N a = x mod u\<rbrakk> \<Longrightarrow> \<exists>ks. length ks = 8 \<and> 3 < peval B' (push_list a ks) \<and> Suc (peval B' (push_list a ks) * push_list a ks 3 * push_list a ks 2) = (push_list a ks 3)\<^sup>2 + (push_list a ks 2)\<^sup>2 \<and> Suc (peval B' (push_list a ks) * push_list a ks (Suc 0) * push_list a ks 0) = (push_list a ks (Suc 0))\<^sup>2 + (push_list a ks 0)\<^sup>2 \<and> push_list a ks 0 < push_list a ks (Suc 0) \<and> (push_list a ks 3)\<^sup>2 dvd push_list a ks (Suc 0) \<and> push_list a ks 4 + 2 * push_list a ks 0 = peval B' (push_list a ks) * push_list a ks (Suc 0) \<and> peval B' (push_list a ks) mod push_list a ks 4 = push_list a ks 5 mod push_list a ks 4 \<and> 2 mod push_list a ks 3 = push_list a ks 5 mod push_list a ks 3 \<and> 2 < push_list a ks 5 \<and> Suc (push_list a ks 5 * push_list a ks 6 * push_list a ks 7) = (push_list a ks 6)\<^sup>2 + (push_list a ks 7)\<^sup>2 \<and> 2 * peval X' (push_list a ks) < push_list a ks 3 \<and> 2 * peval X' (push_list a ks) < push_list a ks 4 \<and> push_list a ks 6 mod push_list a ks 4 = peval X' (push_list a ks) mod push_list a ks 4 \<and> 2 * peval N' (push_list a ks) < push_list a ks 3 \<and> push_list a ks 6 mod push_list a ks 3 = peval N' (push_list a ks) mod push_list a ks 3
[PROOF STEP]
apply (rule exI[of _ "[r, s, t, u, v, w, x, y]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 < peval B a; u\<^sup>2 + t\<^sup>2 = Suc (peval B a * u * t); s\<^sup>2 + r\<^sup>2 = Suc (peval B a * s * r); r < s; u\<^sup>2 dvd s; v + 2 * r = peval B a * s; w mod v = peval B a mod v; w mod u = 2 mod u; 2 < w; x\<^sup>2 + y\<^sup>2 = Suc (w * x * y); 2 * (x mod v) < u; 2 * (x mod v) < v; peval X a = x mod v; 2 * (x mod u) < u; peval N a = x mod u\<rbrakk> \<Longrightarrow> length [r, s, t, u, v, w, x, y] = 8 \<and> 3 < peval B' (push_list a [r, s, t, u, v, w, x, y]) \<and> Suc (peval B' (push_list a [r, s, t, u, v, w, x, y]) * push_list a [r, s, t, u, v, w, x, y] 3 * push_list a [r, s, t, u, v, w, x, y] 2) = (push_list a [r, s, t, u, v, w, x, y] 3)\<^sup>2 + (push_list a [r, s, t, u, v, w, x, y] 2)\<^sup>2 \<and> Suc (peval B' (push_list a [r, s, t, u, v, w, x, y]) * push_list a [r, s, t, u, v, w, x, y] (Suc 0) * push_list a [r, s, t, u, v, w, x, y] 0) = (push_list a [r, s, t, u, v, w, x, y] (Suc 0))\<^sup>2 + (push_list a [r, s, t, u, v, w, x, y] 0)\<^sup>2 \<and> push_list a [r, s, t, u, v, w, x, y] 0 < push_list a [r, s, t, u, v, w, x, y] (Suc 0) \<and> (push_list a [r, s, t, u, v, w, x, y] 3)\<^sup>2 dvd push_list a [r, s, t, u, v, w, x, y] (Suc 0) \<and> push_list a [r, s, t, u, v, w, x, y] 4 + 2 * push_list a [r, s, t, u, v, w, x, y] 0 = peval B' (push_list a [r, s, t, u, v, w, x, y]) * push_list a [r, s, t, u, v, w, x, y] (Suc 0) \<and> peval B' (push_list a [r, s, t, u, v, w, x, y]) mod push_list a [r, s, t, u, v, w, x, y] 4 = push_list a [r, s, t, u, v, w, x, y] 5 mod push_list a [r, s, t, u, v, w, x, y] 4 \<and> 2 mod push_list a [r, s, t, u, v, w, x, y] 3 = push_list a [r, s, t, u, v, w, x, y] 5 mod push_list a [r, s, t, u, v, w, x, y] 3 \<and> 2 < push_list a [r, s, t, u, v, w, x, y] 5 \<and> Suc (push_list a [r, s, t, u, v, w, x, y] 5 * push_list a [r, s, t, u, v, w, x, y] 6 * push_list a [r, s, t, u, v, w, x, y] 7) = (push_list a [r, s, t, u, v, w, x, y] 6)\<^sup>2 + (push_list a [r, s, t, u, v, w, x, y] 7)\<^sup>2 \<and> 2 * peval X' (push_list a [r, s, t, u, v, w, x, y]) < push_list a [r, s, t, u, v, w, x, y] 3 \<and> 2 * peval X' (push_list a [r, s, t, u, v, w, x, y]) < push_list a [r, s, t, u, v, w, x, y] 4 \<and> push_list a [r, s, t, u, v, w, x, y] 6 mod push_list a [r, s, t, u, v, w, x, y] 4 = peval X' (push_list a [r, s, t, u, v, w, x, y]) mod push_list a [r, s, t, u, v, w, x, y] 4 \<and> 2 * peval N' (push_list a [r, s, t, u, v, w, x, y]) < push_list a [r, s, t, u, v, w, x, y] 3 \<and> push_list a [r, s, t, u, v, w, x, y] 6 mod push_list a [r, s, t, u, v, w, x, y] 3 = peval N' (push_list a [r, s, t, u, v, w, x, y]) mod push_list a [r, s, t, u, v, w, x, y] 3
[PROOF STEP]
unfolding pushed_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3 < peval B a; u\<^sup>2 + t\<^sup>2 = Suc (peval B a * u * t); s\<^sup>2 + r\<^sup>2 = Suc (peval B a * s * r); r < s; u\<^sup>2 dvd s; v + 2 * r = peval B a * s; w mod v = peval B a mod v; w mod u = 2 mod u; 2 < w; x\<^sup>2 + y\<^sup>2 = Suc (w * x * y); 2 * (x mod v) < u; 2 * (x mod v) < v; peval X a = x mod v; 2 * (x mod u) < u; peval N a = x mod u\<rbrakk> \<Longrightarrow> length [r, s, t, u, v, w, x, y] = 8 \<and> 3 < peval (push_param B 8) (push_list a [r, s, t, u, v, w, x, y]) \<and> Suc (peval (push_param B 8) (push_list a [r, s, t, u, v, w, x, y]) * push_list a [r, s, t, u, v, w, x, y] 3 * push_list a [r, s, t, u, v, w, x, y] 2) = (push_list a [r, s, t, u, v, w, x, y] 3)\<^sup>2 + (push_list a [r, s, t, u, v, w, x, y] 2)\<^sup>2 \<and> Suc (peval (push_param B 8) (push_list a [r, s, t, u, v, w, x, y]) * push_list a [r, s, t, u, v, w, x, y] (Suc 0) * push_list a [r, s, t, u, v, w, x, y] 0) = (push_list a [r, s, t, u, v, w, x, y] (Suc 0))\<^sup>2 + (push_list a [r, s, t, u, v, w, x, y] 0)\<^sup>2 \<and> push_list a [r, s, t, u, v, w, x, y] 0 < push_list a [r, s, t, u, v, w, x, y] (Suc 0) \<and> (push_list a [r, s, t, u, v, w, x, y] 3)\<^sup>2 dvd push_list a [r, s, t, u, v, w, x, y] (Suc 0) \<and> push_list a [r, s, t, u, v, w, x, y] 4 + 2 * push_list a [r, s, t, u, v, w, x, y] 0 = peval (push_param B 8) (push_list a [r, s, t, u, v, w, x, y]) * push_list a [r, s, t, u, v, w, x, y] (Suc 0) \<and> peval (push_param B 8) (push_list a [r, s, t, u, v, w, x, y]) mod push_list a [r, s, t, u, v, w, x, y] 4 = push_list a [r, s, t, u, v, w, x, y] 5 mod push_list a [r, s, t, u, v, w, x, y] 4 \<and> 2 mod push_list a [r, s, t, u, v, w, x, y] 3 = push_list a [r, s, t, u, v, w, x, y] 5 mod push_list a [r, s, t, u, v, w, x, y] 3 \<and> 2 < push_list a [r, s, t, u, v, w, x, y] 5 \<and> Suc (push_list a [r, s, t, u, v, w, x, y] 5 * push_list a [r, s, t, u, v, w, x, y] 6 * push_list a [r, s, t, u, v, w, x, y] 7) = (push_list a [r, s, t, u, v, w, x, y] 6)\<^sup>2 + (push_list a [r, s, t, u, v, w, x, y] 7)\<^sup>2 \<and> 2 * peval (push_param X 8) (push_list a [r, s, t, u, v, w, x, y]) < push_list a [r, s, t, u, v, w, x, y] 3 \<and> 2 * peval (push_param X 8) (push_list a [r, s, t, u, v, w, x, y]) < push_list a [r, s, t, u, v, w, x, y] 4 \<and> push_list a [r, s, t, u, v, w, x, y] 6 mod push_list a [r, s, t, u, v, w, x, y] 4 = peval (push_param X 8) (push_list a [r, s, t, u, v, w, x, y]) mod push_list a [r, s, t, u, v, w, x, y] 4 \<and> 2 * peval (push_param N 8) (push_list a [r, s, t, u, v, w, x, y]) < push_list a [r, s, t, u, v, w, x, y] 3 \<and> push_list a [r, s, t, u, v, w, x, y] 6 mod push_list a [r, s, t, u, v, w, x, y] 3 = peval (push_param N 8) (push_list a [r, s, t, u, v, w, x, y]) mod push_list a [r, s, t, u, v, w, x, y] 3
[PROOF STEP]
by (auto simp add: push_push[where ?n = 8] push_list_eval)
[PROOF STATE]
proof (state)
this:
eval DR a

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval D a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval D a
[PROOF STEP]
assume "eval DR a"
[PROOF STATE]
proof (state)
this:
eval DR a

goal (1 subgoal):
 1. eval DR a \<Longrightarrow> eval D a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval DR a
[PROOF STEP]
show "eval D a"
[PROOF STATE]
proof (prove)
using this:
eval DR a

goal (1 subgoal):
 1. eval D a
[PROOF STEP]
(* simplify "eval DR a" and undo all the pushes *)
[PROOF STATE]
proof (prove)
using this:
eval DR a

goal (1 subgoal):
 1. eval D a
[PROOF STEP]
unfolding DR_def DR_defs defs param_defs
[PROOF STATE]
proof (prove)
using this:
eval ([\<exists>8] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 3, B'] [\<and>] NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Const 1 [+] B' [*] polynomial.Param 3 [*] polynomial.Param 2, polynomial.Param 3 [^2] [+] polynomial.Param 2 [^2]] [\<and>] (NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Const 1 [+] B' [*] polynomial.Param 1 [*] polynomial.Param 0, polynomial.Param 1 [^2] [+] polynomial.Param 0 [^2]] [\<and>] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Param 0, polynomial.Param 1]) [\<and>] (NARY (\<lambda>l. l ! 0 dvd l ! 1) [polynomial.Param 3 [^2], polynomial.Param 1] [\<and>] NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Param 4 [+] polynomial.Const 2 [*] polynomial.Param 0, B' [*] polynomial.Param 1]) [\<and>] (NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [B', polynomial.Param 4, polynomial.Param 5] [\<and>] NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [polynomial.Const 2, polynomial.Param 3, polynomial.Param 5] [\<and>] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 2, polynomial.Param 5]) [\<and>] NARY (\<lambda>l. l ! 0 = l ! 1) [polynomial.Const 1 [+] polynomial.Param 5 [*] polynomial.Param 6 [*] polynomial.Param 7, polynomial.Param 6 [^2] [+] polynomial.Param 7 [^2]] [\<and>] (NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 2 [*] X', polynomial.Param 3] [\<and>] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 2 [*] X', polynomial.Param 4] [\<and>] NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [polynomial.Param 6, polynomial.Param 4, X'] [\<and>] NARY (\<lambda>l. l ! 0 < l ! 1) [polynomial.Const 2 [*] N', polynomial.Param 3] [\<and>] NARY (\<lambda>l. l ! 0 mod l ! 1 = l ! 2 mod l ! 1) [polynomial.Param 6, polynomial.Param 3, N'])) a

goal (1 subgoal):
 1. eval D a
[PROOF STEP]
apply (auto simp: sq_p_eval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ks. \<lbrakk>length ks = 8; 3 < peval B' (push_list a ks); Suc (peval B' (push_list a ks) * push_list a ks 3 * push_list a ks 2) = (push_list a ks 3)\<^sup>2 + (push_list a ks 2)\<^sup>2; Suc (peval B' (push_list a ks) * push_list a ks (Suc 0) * push_list a ks 0) = (push_list a ks (Suc 0))\<^sup>2 + (push_list a ks 0)\<^sup>2; push_list a ks 0 < push_list a ks (Suc 0); (push_list a ks 3)\<^sup>2 dvd push_list a ks (Suc 0); push_list a ks 4 + 2 * push_list a ks 0 = peval B' (push_list a ks) * push_list a ks (Suc 0); peval B' (push_list a ks) mod push_list a ks 4 = push_list a ks 5 mod push_list a ks 4; 2 mod push_list a ks 3 = push_list a ks 5 mod push_list a ks 3; 2 < push_list a ks 5; Suc (push_list a ks 5 * push_list a ks 6 * push_list a ks 7) = (push_list a ks 6)\<^sup>2 + (push_list a ks 7)\<^sup>2; 2 * peval X' (push_list a ks) < push_list a ks 3; 2 * peval X' (push_list a ks) < push_list a ks 4; push_list a ks 6 mod push_list a ks 4 = peval X' (push_list a ks); 2 * peval N' (push_list a ks) < push_list a ks 3; push_list a ks 6 mod push_list a ks 3 = peval N' (push_list a ks)\<rbrakk> \<Longrightarrow> eval D a
[PROOF STEP]
unfolding pushed_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ks. \<lbrakk>length ks = 8; 3 < peval (push_param B 8) (push_list a ks); Suc (peval (push_param B 8) (push_list a ks) * push_list a ks 3 * push_list a ks 2) = (push_list a ks 3)\<^sup>2 + (push_list a ks 2)\<^sup>2; Suc (peval (push_param B 8) (push_list a ks) * push_list a ks (Suc 0) * push_list a ks 0) = (push_list a ks (Suc 0))\<^sup>2 + (push_list a ks 0)\<^sup>2; push_list a ks 0 < push_list a ks (Suc 0); (push_list a ks 3)\<^sup>2 dvd push_list a ks (Suc 0); push_list a ks 4 + 2 * push_list a ks 0 = peval (push_param B 8) (push_list a ks) * push_list a ks (Suc 0); peval (push_param B 8) (push_list a ks) mod push_list a ks 4 = push_list a ks 5 mod push_list a ks 4; 2 mod push_list a ks 3 = push_list a ks 5 mod push_list a ks 3; 2 < push_list a ks 5; Suc (push_list a ks 5 * push_list a ks 6 * push_list a ks 7) = (push_list a ks 6)\<^sup>2 + (push_list a ks 7)\<^sup>2; 2 * peval (push_param X 8) (push_list a ks) < push_list a ks 3; 2 * peval (push_param X 8) (push_list a ks) < push_list a ks 4; push_list a ks 6 mod push_list a ks 4 = peval (push_param X 8) (push_list a ks); 2 * peval (push_param N 8) (push_list a ks) < push_list a ks 3; push_list a ks 6 mod push_list a ks 3 = peval (push_param N 8) (push_list a ks)\<rbrakk> \<Longrightarrow> eval D a
[PROOF STEP]
apply (auto simp add: push_push[where ?n = 8] push_list_eval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ks. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> eval D a
[PROOF STEP]
(* simplify "eval D a" using the above fact h *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ks. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> eval D a
[PROOF STEP]
unfolding h Exp_Matrices.alpha_equations_def evaled_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ks. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>r s t u v w x y. 3 < peval B a \<and> u\<^sup>2 + t\<^sup>2 = 1 + peval B a * u * t \<and> s\<^sup>2 + r\<^sup>2 = 1 + peval B a * s * r \<and> r < s \<and> u\<^sup>2 dvd s \<and> v + 2 * r = peval B a * s \<and> w mod v = peval B a mod v \<and> w mod u = 2 mod u \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < u \<and> 2 * peval X a < v \<and> peval X a mod v = x mod v \<and> 2 * peval N a < u \<and> peval N a mod u = x mod u
[PROOF STEP]
subgoal for ks
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>r s t u v w x y. 3 < peval B a \<and> u\<^sup>2 + t\<^sup>2 = 1 + peval B a * u * t \<and> s\<^sup>2 + r\<^sup>2 = 1 + peval B a * s * r \<and> r < s \<and> u\<^sup>2 dvd s \<and> v + 2 * r = peval B a * s \<and> w mod v = peval B a mod v \<and> w mod u = 2 mod u \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < u \<and> 2 * peval X a < v \<and> peval X a mod v = x mod v \<and> 2 * peval N a < u \<and> peval N a mod u = x mod u
[PROOF STEP]
apply (rule exI[of _ "ks!0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>s t u v w x y. 3 < peval B a \<and> u\<^sup>2 + t\<^sup>2 = 1 + peval B a * u * t \<and> s\<^sup>2 + (ks ! 0)\<^sup>2 = 1 + peval B a * s * ks ! 0 \<and> ks ! 0 < s \<and> u\<^sup>2 dvd s \<and> v + 2 * ks ! 0 = peval B a * s \<and> w mod v = peval B a mod v \<and> w mod u = 2 mod u \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < u \<and> 2 * peval X a < v \<and> peval X a mod v = x mod v \<and> 2 * peval N a < u \<and> peval N a mod u = x mod u
[PROOF STEP]
apply (rule exI[of _ "ks!1"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>t u v w x y. 3 < peval B a \<and> u\<^sup>2 + t\<^sup>2 = 1 + peval B a * u * t \<and> (ks ! 1)\<^sup>2 + (ks ! 0)\<^sup>2 = 1 + peval B a * ks ! 1 * ks ! 0 \<and> ks ! 0 < ks ! 1 \<and> u\<^sup>2 dvd ks ! 1 \<and> v + 2 * ks ! 0 = peval B a * ks ! 1 \<and> w mod v = peval B a mod v \<and> w mod u = 2 mod u \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < u \<and> 2 * peval X a < v \<and> peval X a mod v = x mod v \<and> 2 * peval N a < u \<and> peval N a mod u = x mod u
[PROOF STEP]
apply (rule exI[of _ "ks!2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>u v w x y. 3 < peval B a \<and> u\<^sup>2 + (ks ! 2)\<^sup>2 = 1 + peval B a * u * ks ! 2 \<and> (ks ! 1)\<^sup>2 + (ks ! 0)\<^sup>2 = 1 + peval B a * ks ! 1 * ks ! 0 \<and> ks ! 0 < ks ! 1 \<and> u\<^sup>2 dvd ks ! 1 \<and> v + 2 * ks ! 0 = peval B a * ks ! 1 \<and> w mod v = peval B a mod v \<and> w mod u = 2 mod u \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < u \<and> 2 * peval X a < v \<and> peval X a mod v = x mod v \<and> 2 * peval N a < u \<and> peval N a mod u = x mod u
[PROOF STEP]
apply (rule exI[of _ "ks!3"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>v w x y. 3 < peval B a \<and> (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2 = 1 + peval B a * ks ! 3 * ks ! 2 \<and> (ks ! 1)\<^sup>2 + (ks ! 0)\<^sup>2 = 1 + peval B a * ks ! 1 * ks ! 0 \<and> ks ! 0 < ks ! 1 \<and> (ks ! 3)\<^sup>2 dvd ks ! 1 \<and> v + 2 * ks ! 0 = peval B a * ks ! 1 \<and> w mod v = peval B a mod v \<and> w mod ks ! 3 = 2 mod ks ! 3 \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < ks ! 3 \<and> 2 * peval X a < v \<and> peval X a mod v = x mod v \<and> 2 * peval N a < ks ! 3 \<and> peval N a mod ks ! 3 = x mod ks ! 3
[PROOF STEP]
apply (rule exI[of _ "ks!4"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>w x y. 3 < peval B a \<and> (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2 = 1 + peval B a * ks ! 3 * ks ! 2 \<and> (ks ! 1)\<^sup>2 + (ks ! 0)\<^sup>2 = 1 + peval B a * ks ! 1 * ks ! 0 \<and> ks ! 0 < ks ! 1 \<and> (ks ! 3)\<^sup>2 dvd ks ! 1 \<and> ks ! 4 + 2 * ks ! 0 = peval B a * ks ! 1 \<and> w mod ks ! 4 = peval B a mod ks ! 4 \<and> w mod ks ! 3 = 2 mod ks ! 3 \<and> 2 < w \<and> x\<^sup>2 + y\<^sup>2 = 1 + w * x * y \<and> 2 * peval X a < ks ! 3 \<and> 2 * peval X a < ks ! 4 \<and> peval X a mod ks ! 4 = x mod ks ! 4 \<and> 2 * peval N a < ks ! 3 \<and> peval N a mod ks ! 3 = x mod ks ! 3
[PROOF STEP]
apply (rule exI[of _ "ks!5"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>x y. 3 < peval B a \<and> (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2 = 1 + peval B a * ks ! 3 * ks ! 2 \<and> (ks ! 1)\<^sup>2 + (ks ! 0)\<^sup>2 = 1 + peval B a * ks ! 1 * ks ! 0 \<and> ks ! 0 < ks ! 1 \<and> (ks ! 3)\<^sup>2 dvd ks ! 1 \<and> ks ! 4 + 2 * ks ! 0 = peval B a * ks ! 1 \<and> ks ! 5 mod ks ! 4 = peval B a mod ks ! 4 \<and> ks ! 5 mod ks ! 3 = 2 mod ks ! 3 \<and> 2 < ks ! 5 \<and> x\<^sup>2 + y\<^sup>2 = 1 + ks ! 5 * x * y \<and> 2 * peval X a < ks ! 3 \<and> 2 * peval X a < ks ! 4 \<and> peval X a mod ks ! 4 = x mod ks ! 4 \<and> 2 * peval N a < ks ! 3 \<and> peval N a mod ks ! 3 = x mod ks ! 3
[PROOF STEP]
apply (rule exI[of _ "ks!6"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> \<exists>y. 3 < peval B a \<and> (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2 = 1 + peval B a * ks ! 3 * ks ! 2 \<and> (ks ! 1)\<^sup>2 + (ks ! 0)\<^sup>2 = 1 + peval B a * ks ! 1 * ks ! 0 \<and> ks ! 0 < ks ! 1 \<and> (ks ! 3)\<^sup>2 dvd ks ! 1 \<and> ks ! 4 + 2 * ks ! 0 = peval B a * ks ! 1 \<and> ks ! 5 mod ks ! 4 = peval B a mod ks ! 4 \<and> ks ! 5 mod ks ! 3 = 2 mod ks ! 3 \<and> 2 < ks ! 5 \<and> (ks ! 6)\<^sup>2 + y\<^sup>2 = 1 + ks ! 5 * ks ! 6 * y \<and> 2 * peval X a < ks ! 3 \<and> 2 * peval X a < ks ! 4 \<and> peval X a mod ks ! 4 = ks ! 6 mod ks ! 4 \<and> 2 * peval N a < ks ! 3 \<and> peval N a mod ks ! 3 = ks ! 6 mod ks ! 3
[PROOF STEP]
apply (rule exI[of _ "ks!7"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ks = 8; 3 < peval B a; Suc (peval B a * ks ! 3 * ks ! 2) = (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2; Suc (peval B a * ks ! Suc 0 * ks ! 0) = (ks ! Suc 0)\<^sup>2 + (ks ! 0)\<^sup>2; ks ! 0 < ks ! Suc 0; (ks ! 3)\<^sup>2 dvd ks ! Suc 0; ks ! 4 + 2 * ks ! 0 = peval B a * ks ! Suc 0; peval B a mod ks ! 4 = ks ! 5 mod ks ! 4; 2 mod ks ! 3 = ks ! 5 mod ks ! 3; 2 < ks ! 5; Suc (ks ! 5 * ks ! 6 * ks ! 7) = (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2; 2 * peval X a < ks ! 3; 2 * peval X a < ks ! 4; ks ! 6 mod ks ! 4 = peval X a; 2 * peval N a < ks ! 3; ks ! 6 mod ks ! 3 = peval N a\<rbrakk> \<Longrightarrow> 3 < peval B a \<and> (ks ! 3)\<^sup>2 + (ks ! 2)\<^sup>2 = 1 + peval B a * ks ! 3 * ks ! 2 \<and> (ks ! 1)\<^sup>2 + (ks ! 0)\<^sup>2 = 1 + peval B a * ks ! 1 * ks ! 0 \<and> ks ! 0 < ks ! 1 \<and> (ks ! 3)\<^sup>2 dvd ks ! 1 \<and> ks ! 4 + 2 * ks ! 0 = peval B a * ks ! 1 \<and> ks ! 5 mod ks ! 4 = peval B a mod ks ! 4 \<and> ks ! 5 mod ks ! 3 = 2 mod ks ! 3 \<and> 2 < ks ! 5 \<and> (ks ! 6)\<^sup>2 + (ks ! 7)\<^sup>2 = 1 + ks ! 5 * ks ! 6 * ks ! 7 \<and> 2 * peval X a < ks ! 3 \<and> 2 * peval X a < ks ! 4 \<and> peval X a mod ks ! 4 = ks ! 6 mod ks ! 4 \<and> 2 * peval N a < ks ! 3 \<and> peval N a mod ks ! 3 = ks ! 6 mod ks ! 3
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval D a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval D a = eval DR a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval D ?a = eval DR ?a

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_dioph_rel DR
eval D ?a = eval DR ?a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_dioph_rel DR
eval D ?a = eval DR ?a

goal (1 subgoal):
 1. is_dioph_rel D
[PROOF STEP]
by (auto simp: is_dioph_rel_def)
[PROOF STATE]
proof (state)
this:
is_dioph_rel D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_in_doubt_allow: "wf_unknown_match_tac in_doubt_allow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_unknown_match_tac in_doubt_allow
[PROOF STEP]
unfolding wf_unknown_match_tac_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_doubt_allow Drop = in_doubt_allow Reject
[PROOF STEP]
by(simp add: fun_eq_iff)


[STATEMENT]
lemma wf_in_doubt_deny: "wf_unknown_match_tac in_doubt_deny"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_unknown_match_tac in_doubt_deny
[PROOF STEP]
unfolding wf_unknown_match_tac_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_doubt_deny Drop = in_doubt_deny Reject
[PROOF STEP]
by(simp add: fun_eq_iff)


[STATEMENT]
lemma packet_independent_unknown_match_tacs:
    "packet_independent_\<alpha> in_doubt_allow"
    "packet_independent_\<alpha> in_doubt_deny"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. packet_independent_\<alpha> in_doubt_allow &&& packet_independent_\<alpha> in_doubt_deny
[PROOF STEP]
by(simp_all add: packet_independent_\<alpha>_def)


[STATEMENT]
lemma Drop_neq_Accept_unknown_match_tacs:
      "in_doubt_allow Drop \<noteq> in_doubt_allow Accept"
      "in_doubt_deny Drop \<noteq> in_doubt_deny Accept"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_doubt_allow Drop \<noteq> in_doubt_allow Accept &&& in_doubt_deny Drop \<noteq> in_doubt_deny Accept
[PROOF STEP]
by(simp_all add: fun_eq_iff)


[STATEMENT]
lemma T1_1[semantics]:
    "(w \<Turnstile> \<lparr>F,x\<rparr>) = (\<exists> r o\<^sub>1 . Some r = d\<^sub>1 F \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> o\<^sub>1 \<in> ex1 r w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lparr>F,x\<rparr>) = (\<exists>r o\<^sub>1. Some r = d\<^sub>1 F \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> o\<^sub>1 \<in> ex1 r w)
[PROOF STEP]
unfolding semantics_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lparr>F,x\<rparr>) = (\<exists>r o\<^sub>1. Some r = map_fun eval\<Pi>\<^sub>1 id Some F \<and> Some o\<^sub>1 = map_fun eval\<kappa> id id x \<and> o\<^sub>1 \<in> {x. r (\<nu>\<upsilon> x) dj w})
[PROOF STEP]
apply (simp add: meta_defs meta_aux rep_def proper_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (None \<noteq> eval\<kappa> x \<and> eval\<Pi>\<^sub>1 F (\<nu>\<upsilon> (the (eval\<kappa> x))) dj w) = (\<exists>o\<^sub>1. Some o\<^sub>1 = eval\<kappa> x \<and> eval\<Pi>\<^sub>1 F (\<nu>\<upsilon> o\<^sub>1) dj w)
[PROOF STEP]
by (metis option.discI option.exhaust option.sel)


[STATEMENT]
lemma T1_2[semantics]:
    "(w \<Turnstile> \<lparr>F,x,y\<rparr>) = (\<exists> r o\<^sub>1 o\<^sub>2 . Some r = d\<^sub>2 F \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x
                               \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<and> (o\<^sub>1, o\<^sub>2) \<in> ex2 r w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lparr>F,x,y\<rparr>) = (\<exists>r o\<^sub>1 o\<^sub>2. Some r = d\<^sub>2 F \<and> Some o\<^sub>1 = d\<^sub>\<kappa> x \<and> Some o\<^sub>2 = d\<^sub>\<kappa> y \<and> (o\<^sub>1, o\<^sub>2) \<in> ex2 r w)
[PROOF STEP]
unfolding semantics_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<Turnstile> \<lparr>F,x,y\<rparr>) = (\<exists>r o\<^sub>1 o\<^sub>2. Some r = map_fun eval\<Pi>\<^sub>2 id Some F \<and> Some o\<^sub>1 = map_fun eval\<kappa> id id x \<and> Some o\<^sub>2 = map_fun eval\<kappa> id id y \<and> (o\<^sub>1, o\<^sub>2) \<in> {(x, y). r (\<nu>\<upsilon> x) (\<nu>\<upsilon> y) dj w})
[PROOF STEP]
apply (simp add: meta_defs meta_aux rep_def proper_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (None \<noteq> eval\<kappa> x \<and> None \<noteq> eval\<kappa> y \<and> eval\<Pi>\<^sub>2 F (\<nu>\<upsilon> (the (eval\<kappa> x))) (\<nu>\<upsilon> (the (eval\<kappa> y))) dj w) = (\<exists>o\<^sub>1. Some o\<^sub>1 = eval\<kappa> x \<and> (\<exists>o\<^sub>2. Some o\<^sub>2 = eval\<kappa> y \<and> eval\<Pi>\<^sub>2 F (\<nu>\<upsilon> o\<^sub>1) (\<nu>\<upsilon> o\<^sub>2) dj w))
[PROOF STEP]
by (metis option.discI option.exhaust option.sel)