# Theory Up

theory Up
imports UpDown_Scheme Triangular_Function
section

theory Up
imports UpDown_Scheme Triangular_Function
begin

lemma up'_inplace:
assumes p'_in:  and
shows
using p'_in
proof (induct l arbitrary: p α)
case (Suc l)
let  =
let  =
let  =

from contrapos_nn[OF  grid_child[OF ]]
have left:  and
right:  by auto

have  using grid.Start Suc.prems by auto
with Suc.hyps[OF left, of α] Suc.hyps[OF right, of ?upl]
show ?case
by (cases , cases , auto simp add: Let_def)
qed auto

lemma up'_fl_fr:

proof (induct lm arbitrary: p p_l p_r α)
case (Suc lm)
note [simp]

from child_ex_neighbour
obtain pc_r pc_l
where pc_r_def:
and pc_l_def:  by blast

define pc where  for dir
{ fix dir have
by (cases dir, auto simp add: pc_def pc_r_def pc_l_def) } note pc_child = this
{ fix dir have
by (cases dir, auto simp add: pc_def pc_r_def pc_l_def) } note pc_child_inv = this
hence  by auto
hence  by auto
hence [simp]:  by auto

let ?l =
let ?C =
let ?sum' =
let ?sum =
let ?ch =
let ?f =
let ?fm =
let ?result =
let ?up =

define βl where
define βr where

define p_d where  for dir
have p_d_child:  for dir
using Suc.prems p_d_def by (cases dir) auto
hence  by auto
hence  by auto

{ fix dir

{ fix p' assume
hence
using l2_zigzag[OF _ p_d_child[of dir] _ pc_child[of dir]]
by (cases dir) (auto simp add: algebra_simps) }
hence inv_dir_sum:
by (auto simp add: sum.distrib[symmetric] sum_divide_distrib)

have
using l2_down2[OF _ _ ]
by (force intro!: sum.cong simp add: sum_divide_distrib)
moreover
have
using l2_child[OF , of p dir ] p_d_child[of dir]
child_lv child_ix grid.Start[of p ]
ultimately
have
using lgrid_sum[where b=p] and child_level and inv_dir_sum
by (cases dir) auto
hence
by (cases dir) auto }
note this[of left] this[of right]
moreover
note eq = up'_inplace[OF grid_not_child[OF ], of d  lm]
{ fix p' assume
with grid_disjunct[of d p] up'_inplace[of p'   d lm α] βl_def
have  by auto }
hence
using βl_def pc_child_inv[of left] pc_child_inv[of right]
Suc.hyps[of   p α] eq[of left α]
Suc.hyps[of  p  βl] eq[of right βl]
by (cases , cases ) (simp add: Let_def)
ultimately show ?case by (auto simp add: p_d_def)
next
case 0
show ?case by simp
qed

lemma up'_β:

(is )
proof (induct l arbitrary: b p α)
case (Suc l)

let ?l =  and ?r =
obtain p_l where p_l_def:  using child_ex_neighbour[where dir=right] by auto
obtain p_r where p_r_def:  using child_ex_neighbour[where dir=left] by auto

let ?ul =
let ?ur =

let  =
let  =

from  have  unfolding sparsegrid'_def start_def
by auto
hence  using  by auto

{ fix p' assume
hence
using grid_disjunct[OF ] by auto
hence  using up'_inplace by auto
} note eq = this

show
proof (cases )
case True

let  =
let  =

have  using  by auto
from up'_fl_fr[OF this p_r_def]
have fml:  by simp

have  using  by auto
from up'_fl_fr[OF this _ p_l_def, where α=]
have fmr:  by simp

have  using  by auto
hence  unfolding lgrid_def by auto
from sum_diff[OF lgrid_finite this]
have  by simp
also have
using lgrid_sum and  and  by auto
also have  using fml and fmr
and  and child_level[OF ]
using eq unfolding True lgrid_def by auto

finally show ?thesis unfolding up'.simps Let_def and fun_upd_def lgrid_def
using  and
by (cases ?ul, cases ?ur, auto)
next
case False

have  and
using  and  unfolding sparsegrid'_def by auto
from Suc.hyps[OF _ _ this(1)] Suc.hyps[OF _ _ this(2)]
have  and
using  and  and  by auto

show ?thesis
proof (cases )
case True
hence  and  unfolding lgrid_def by auto
hence
unfolding grid_partition[of b] using  by auto
thus ?thesis
proof (rule disjE)
assume
hence
using grid_disjunct[OF ] by auto
thus ?thesis
using  and
using
unfolding lgrid_def grid_partition[of b]
by (cases ?ul, cases ?ur, auto simp add: Let_def)
next
assume *:
hence
using grid_disjunct[OF ] by auto
moreover
{ fix p' assume
from grid_transitive[OF this *] eq[of p']
have  by simp
}
ultimately show ?thesis
using  and
using   *
unfolding lgrid_def
by (cases ?ul, cases ?ur, auto simp add: Let_def)
qed
next
case False
then have  and
unfolding lgrid_def and grid_partition[where p=b] by auto
with False show ?thesis using  and
using
unfolding lgrid_def
by (cases ?ul, cases ?ur, auto simp add: Let_def)
qed
qed
next
case 0
then have
using lgrid_empty'[where p=b and lm=lm and ds=] by auto
with 0 show ?case unfolding up'.simps by auto
qed

lemma up:
assumes  and
shows
proof -
let ?S =
let ?F =

{ fix p b assume
from grid_transitive[OF _ this subset_refl subset_refl]
have
unfolding lgrid_def by auto
} note lgrid_eq = this

{ fix l b p α
assume b:
hence  and  using sparsegrid'_start  by auto
assume l:  and p:
note sparsegridE[OF p]

note up' = up'_β[OF  l  ]

have
proof (cases )
case True with baseE(2)[OF ]
have  and  by auto
show ?thesis
using lgrid_eq[OF ]
unfolding up' if_P[OF True] if_P[OF ]
by (intro sum.mono_neutral_cong_left lgrid_finite) auto
next
case False
moreover have
proof (rule ccontr)
assume
hence  using b by (auto intro!: baseI)
thus False using False by auto
qed
ultimately show ?thesis unfolding up' by auto
qed }
with lift[where F = ?F, OF  ]
have lift_eq:  by auto
from lgrid_eq[OF baseE(2)[OF sparsegrid_subset[OF ]]]
show ?thesis
unfolding up_def lift_eq by (intro sum.mono_neutral_cong_right lgrid_finite) auto
qed

end