Theory Refine_Reachability_Analysis_C1
theory Refine_Reachability_Analysis_C1
imports
Abstract_Reachability_Analysis_C1
Refine_Reachability_Analysis
begin
lemma fst_flow1_of_vec1[simp]: "fst (flow1_of_vec1 x) = fst x"
by (auto simp: flow1_of_vec1_def)
lemma fst_vec1_of_flow[simp]: "fst (vec1_of_flow1 x) = fst x"
by (auto simp: vec1_of_flow1_def)
context approximate_sets_ode'
begin
lemma poincare_mapsto_scaleR2I:
"poincare_mapsto P (scaleR2 x1 x2 baa) UNIV x1b (scaleR2 x1 x2 aca)"
if "poincare_mapsto P (baa) UNIV x1b (aca)"
using that
apply (auto simp: poincare_mapsto_def scaleR2_def image_def vimage_def)
apply (drule bspec, assumption)
apply auto
apply (rule exI, rule conjI, assumption)
apply (rule exI, rule conjI, assumption, rule conjI, assumption)
apply (rule bexI) prefer 2 apply assumption
apply (auto simp: scaleR_blinfun_compose_right)
done
context includes ode_ops.lifting begin
lemma var_safe_form_eq[simp]: "var.safe_form = safe_form"
unfolding var.safe_form_def
by transfer (auto simp: var_ode_ops_def safe_form_def)
lemma var_ode_e: "var.ode_e = ode_e'"
unfolding var.ode_e_def
by transfer (auto simp: var_ode_ops_def)
end
lemma wd_imp_var_wd[refine_vcg, intro]: "wd (TYPE('n rvec)) ⟹ var.wd (TYPE('n::enum vec1))"
unfolding var.wd_def
by (auto simp: wd_def length_concat o_def sum_list_distinct_conv_sum_set
concat_map_map_index var_ode_e D_def ode_e'_def
intro!: max_Var_floatariths_mmult_fa[le] max_Var_floatariths_mapI
max_Var_floatarith_FDERIV_floatarith[le]
max_Var_floatariths_fold_const_fa[le]
max_Var_floatarith_le_max_Var_floatariths_nthI
max_Var_floatariths_list_updateI max_Var_floatariths_replicateI)
lemma safe_eq:
assumes "wd TYPE('n::enum rvec)"
shows "var.Csafe = ((Csafe × UNIV)::'n vec1 set)"
using assms var.wdD[OF wd_imp_var_wd[OF assms]] wdD[OF assms]
unfolding var.safe_def safe_def var.wd_def wd_def var.Csafe_def Csafe_def
unfolding ode_e'_def var_ode_e
apply (auto simp: D_def)
subgoal
apply (subst interpret_form_max_Var_cong) prefer 2 apply assumption
by (auto simp: nth_Basis_list_prod)
subgoal for a b
apply (drule isFDERIV_appendD1)
apply simp apply simp apply (auto intro!: max_Var_floatariths_fold_const_fa[le])[]
apply (rule isFDERIV_max_Var_congI, assumption)
by (auto simp: nth_Basis_list_prod)
subgoal
apply (subst interpret_form_max_Var_cong) prefer 2 apply assumption
by (auto simp: nth_Basis_list_prod)
subgoal for a b
apply (rule isFDERIV_appendI1)
apply (rule isFDERIV_max_Var_congI, assumption)
apply (auto simp: nth_Basis_list_prod)
apply (auto simp: isFDERIV_def FDERIV_floatariths_def in_set_conv_nth isDERIV_inner_iff
length_concat o_def sum_list_distinct_conv_sum_set concat_map_map_index
intro!: isDERIV_FDERIV_floatarith isDERIV_mmult_fa_nth)
apply (rule isDERIV_max_Var_floatarithI[where ys="list_of_eucl a"])
subgoal for i j k
apply (cases "i < CARD('n)")
subgoal by auto
subgoal apply (rule isDERIV_max_VarI)
apply (rule max_Var_floatarith_le_max_Var_floatariths_nthI)
apply force
apply auto
done
done
subgoal for i j k l by (auto dest!: max_Var_floatariths_lessI simp: nth_Basis_list_prod)
subgoal by (auto simp: nth_list_update)
done
done
lemma
var_ode_eq:
fixes x::"'n::enum vec1"
assumes "wd TYPE('n rvec)" and [simp]: "(fst x) ∈ Csafe"
shows "var.ode x = (ode (fst x), matrix (ode_d1 (fst x)) ** snd x)"
proof -
have "interpret_floatariths ode_e (list_of_eucl x) =
interpret_floatariths ode_e (list_of_eucl (fst x))"
apply (rule interpret_floatariths_max_Var_cong)
using wdD[OF ‹wd _›]
by (auto simp: list_of_eucl_nth_if nth_Basis_list_prod inner_prod_def)
moreover
have "eucl_of_list
(interpret_floatariths
(mmult_fa D D D
(concat (map (λj. map (λi. FDERIV_floatarith (ode_e ! j) [0..<D] ((replicate D 0)[i := 1])) [0..<D]) [0..<D]))
(map floatarith.Var [D..<D + D * D])) (list_of_eucl x)) =
matrix (blinfun_apply (ode_d 0 (fst x) 0)) ** snd x"
unfolding matrix_eq
apply auto
apply (subst matrix_vector_mul_assoc[symmetric])
apply (subst matrix_works)
subgoal by (auto simp: linear_matrix_vector_mul_eq
intro!: bounded_linear.linear blinfun.bounded_linear_right)
apply (subst einterpret_mmult_fa[where 'n='n and 'm = 'n and 'l='n])
subgoal by (simp add: wdD[OF ‹wd _›])
subgoal by (simp add: length_concat o_def sum_list_distinct_conv_sum_set wdD[OF ‹wd _›])
subgoal by (simp add: length_concat o_def sum_list_distinct_conv_sum_set wdD[OF ‹wd _›])
subgoal for v
proof -
have v: "einterpret (map floatarith.Var [D..<D + D * D]) (list_of_eucl x) *v v = snd x *v v"
apply (vector matrix_vector_mult_def)
apply (simp add: vec_nth_eq_list_of_eucl2 wdD[OF ‹wd _›])
apply (auto simp: vec_nth_eq_list_of_eucl1 sum_index_enum_eq)
apply (subst sum_index_enum_eq)+
apply (rule sum.cong)
by (auto simp: nth_Basis_list_prod prod_eq_iff inner_prod_def)
show ?thesis
unfolding matrix_vector_mul_assoc[symmetric]
apply (subst v)
apply (auto simp: concat_map_map_index vec_nth_eq_list_of_eucl2)
apply (subst eucl_of_list_list_of_eucl[of "snd x *v v", symmetric])
apply (subst (2) eucl_of_list_list_of_eucl[of "snd x *v v", symmetric])
apply (subst eucl_of_list_matrix_vector_mult_eq_sum_nth_Basis_list)
subgoal by (simp add: length_concat o_def sum_list_distinct_conv_sum_set wdD[OF ‹wd _›])
subgoal by simp
apply (subst blinfun_apply_eq_sum)
apply (auto simp: vec_nth_eq_list_of_eucl1 sum_index_enum_eq)
apply (auto simp: scaleR_sum_left ode_d.rep_eq intro!: sum.cong[OF refl])
apply (auto simp: ode_d_raw_def wdD[OF ‹wd _›] eucl_of_list_inner )
apply (auto simp: ode_d_expr_def FDERIV_floatariths_def wdD[OF ‹wd _›] )
apply (rule interpret_floatarith_FDERIV_floatarith_cong)
subgoal for x y i
using wdD[OF ‹wd _›]
by (auto simp add: nth_append inner_prod_def
nth_Basis_list_prod dest!: max_Var_floatariths_lessI)
subgoal by auto
subgoal by auto
subgoal
apply (auto simp: wdD[OF ‹wd _›] nth_list_update inner_Basis intro!: nth_equalityI)
by (metis ‹length (list_of_eucl (snd x *v v)) = CARD('n)› index_Basis_list_nth length_list_of_eucl)
done
qed
done
ultimately show ?thesis
unfolding var.ode_def ode_def
unfolding ode_e'_def var_ode_e
by (auto simp: wdD[OF ‹wd _›] ode_d1_def intro!: euclidean_eqI[where 'a="'n vec1"])
qed
lemma var_existence_ivl_imp_existence_ivl:
fixes x::"'n::enum vec1"
assumes wd: "wd TYPE('n rvec)"
assumes t: "t ∈ var.existence_ivl0 x"
shows "t ∈ existence_ivl0 (fst x)"
proof (rule existence_ivl_maximal_segment)
from var.flow_solves_ode[OF UNIV_I var.mem_existence_ivl_iv_defined(2), OF t]
have D: "(var.flow0 x solves_ode (λ_. var.ode)) {0--t} (var.Csafe)"
apply (rule solves_ode_on_subset)
apply (rule var.closed_segment_subset_existence_ivl)
apply (rule t)
apply simp
done
show "((λt. fst (var.flow0 x t)) solves_ode (λ_. ode)) {0--t} (Csafe)"
using var.closed_segment_subset_existence_ivl[OF t]
apply (auto simp: has_vderiv_on_def has_vector_derivative_def subset_iff
intro!: solves_odeI derivative_eq_intros)
apply (rule refl)
apply (rule refl)
apply (rule refl)
apply (auto simp: var.flowderiv_def )
apply (subst var_ode_eq[OF wd(1)])
apply (auto simp: blinfun.bilinear_simps)
subgoal for s
using solves_odeD(2)[OF D, of s]
by (subst(asm) (3) safe_eq[OF wd]) (auto )
subgoal for s
using solves_odeD(2)[OF D, of s]
by (subst(asm) (3) safe_eq[OF wd]) (auto )
done
next
show "fst (var.flow0 x 0) = fst x"
apply (subst var.flow_initial_time)
apply simp
apply (rule var.mem_existence_ivl_iv_defined[OF t])
apply auto
done
qed simp
lemma existence_ivl_imp_var_existence_ivl:
fixes x::"'n::enum rvec"
assumes wd: "wd TYPE('n rvec)"
assumes t: "t ∈ existence_ivl0 x"
shows "t ∈ var.existence_ivl0 ((x, W)::'n vec1)"
proof (rule var.existence_ivl_maximal_segment)
from flow_solves_ode[OF UNIV_I mem_existence_ivl_iv_defined(2), OF t]
have D: "(flow0 x solves_ode (λ_. ode)) {0--t} (Csafe)"
apply (rule solves_ode_on_subset)
apply (rule closed_segment_subset_existence_ivl)
apply (rule t)
apply simp
done
show "((λt. (flow0 x t, matrix (Dflow x t) ** W)) solves_ode (λ_. var.ode)) {0--t} (var.Csafe)"
using closed_segment_subset_existence_ivl[OF t]
apply (auto simp: has_vderiv_on_def has_vector_derivative_def subset_iff
intro!: solves_odeI derivative_eq_intros)
apply (rule refl)
apply (rule refl)
apply (rule refl)
apply (rule has_derivative_at_withinI)
apply (rule Dflow_has_derivative)
apply force
apply (rule refl)
apply (auto simp: flowderiv_def )
apply (subst var_ode_eq)
apply (auto simp: blinfun.bilinear_simps matrix_blinfun_compose wd
intro!: ext)
subgoal for s h
unfolding matrix_scaleR matrix_blinfun_compose matrix_mul_assoc matrix_scaleR_right ..
subgoal for s
using solves_odeD(2)[OF D, of s] safe_eq[OF wd]
by auto
done
next
have "x ∈ Csafe" by rule fact
then show "(flow0 x 0, matrix (blinfun_apply (Dflow x 0)) ** W) = (x, W)"
apply (auto )
apply (vector matrix_def matrix_matrix_mult_def axis_def)
by (auto simp: if_distrib if_distribR cong: if_cong)
qed auto
theorem var_existence_ivl0_eq_existence_ivl0:
fixes x::"'n::enum vec1"
assumes wd: "wd TYPE('n rvec)"
shows "var.existence_ivl0 (x::'n vec1) = existence_ivl0 (fst x)"
apply safe
subgoal by (rule var_existence_ivl_imp_existence_ivl[OF wd, of _ "x", simplified], simp)
subgoal
by (rule existence_ivl_imp_var_existence_ivl[OF wd, of _ "fst x" "snd x", unfolded prod.collapse])
done
theorem var_flow_eq_flow_Dflow:
fixes x::"'n::enum vec1"
assumes wd: "wd TYPE('n rvec)"
assumes t: "t ∈ var.existence_ivl0 x"
shows "var.flow0 x t = vec1_of_flow1 (flow0 (fst x) t, Dflow (fst x) t o⇩L blinfun_of_vmatrix (snd x)) "
proof -
have x: "x ∈ var.Csafe"
by (rule var.mem_existence_ivl_iv_defined[OF t])
then have "fst x ∈ Csafe"
by (subst (asm) safe_eq[OF wd]) auto
then have sx[simp]: "(fst x) ∈ Csafe" by simp
show ?thesis
proof (rule var.flow_unique_on[OF t])
show "vec1_of_flow1 (flow0 (fst x) 0, Dflow (fst x) 0 o⇩L blinfun_of_vmatrix (snd x)) = x"
by (auto simp: vec1_of_flow1_def x)
show "((λa. vec1_of_flow1 (flow0 (fst x) a, Dflow (fst x) a o⇩L blinfun_of_vmatrix (snd x))) has_vderiv_on
(λt. var.ode (vec1_of_flow1 (flow0 (fst x) t, Dflow (fst x) t o⇩L blinfun_of_vmatrix (snd x)))))
(var.existence_ivl0 x)"
apply (auto simp: has_vderiv_on_def has_vector_derivative_def vec1_of_flow1_def
at_within_open[OF _ var.open_existence_ivl] flowderiv_def
intro!: derivative_eq_intros var_existence_ivl_imp_existence_ivl[OF wd]
Dflow_has_derivative ext)
apply (subst var_ode_eq[OF wd(1)])
apply (auto simp: blinfun.bilinear_simps)
subgoal for t
using flow_in_domain[of t "fst x"]
by (simp add: var_existence_ivl_imp_existence_ivl[OF wd])
subgoal for t h
by (simp add: matrix_blinfun_compose matrix_scaleR matrix_mul_assoc matrix_scaleR_right)
done
fix t
assume "t ∈ var.existence_ivl0 x"
then show "vec1_of_flow1 (flow0 (fst x) t, Dflow (fst x) t o⇩L blinfun_of_vmatrix (snd x)) ∈ var.Csafe"
by (subst safe_eq[OF wd])
(auto simp: vec1_of_flow1_def dest!: var_existence_ivl_imp_existence_ivl[OF wd]
flow_in_domain)
qed
qed
theorem flow_Dflow_eq_var_flow:
fixes x::"'n::enum rvec"
assumes wd: "wd TYPE('n rvec)"
assumes t: "t ∈ existence_ivl0 x"
shows "(flow0 x t, Dflow x t o⇩L W) = flow1_of_vec1 (var.flow0 (x, matrix W) t::'n vec1)"
using var_flow_eq_flow_Dflow[OF wd existence_ivl_imp_var_existence_ivl[OF wd t]]
unfolding var_flow_eq_flow_Dflow[OF wd existence_ivl_imp_var_existence_ivl[OF wd t]]
by (auto simp: flow1_of_vec1_def vec1_of_flow1_def)
context includes blinfun.lifting begin
lemma flow1_of_vec1_vec1_of_flow1[simp]:
"flow1_of_vec1 (vec1_of_flow1 X) = X"
unfolding vec1_of_flow1_def flow1_of_vec1_def
by (transfer) auto
end
lemma
var_flowpipe0_flowpipe:
assumes wd: "wd TYPE('n::enum rvec)"
assumes "var.flowpipe0 X0 hl hu (CX) X1"
assumes "fst ` X0 ⊆ Csafe"
assumes "fst ` CX ⊆ Csafe"
assumes "fst ` X1 ⊆ Csafe"
shows "flowpipe (flow1_of_vec1 ` X0) hl hu (flow1_of_vec1 ` (CX::'n vec1 set)) (flow1_of_vec1 ` X1)"
using assms
unfolding flowpipe_def var.flowpipe0_def
apply safe
subgoal by (auto simp add: flow1_of_vec1_def vec1_of_flow1_def safe_eq[OF wd])
subgoal by (auto simp add: flow1_of_vec1_def vec1_of_flow1_def safe_eq[OF wd])
subgoal by (auto simp add: flow1_of_vec1_def vec1_of_flow1_def safe_eq[OF wd])
subgoal for x W y V h
apply (drule bspec[where x="(y, V)"], force)
apply (drule bspec, assumption)
by (simp add: var_existence_ivl0_eq_existence_ivl0[OF wd] flow1_of_vec1_def)
subgoal for x W y V h
apply (drule bspec[where x="(y, V)"], force)
apply (drule bspec, assumption)
apply (subst flow_Dflow_eq_var_flow[OF wd],
force simp: var_existence_ivl0_eq_existence_ivl0[OF wd] flow1_of_vec1_def)
apply (rule imageI)
by (simp add: vec1_of_flow1_def flow1_of_vec1_def)
subgoal for x W y V h h'
apply (drule bspec[where x="vec1_of_flow1 (x, W)"], force)
apply (drule bspec, assumption)
apply (subst flow_Dflow_eq_var_flow[OF wd])
apply (subst (asm) var_existence_ivl0_eq_existence_ivl0[OF wd])
apply (simp add: flow1_of_vec1_def)
subgoal
by (meson local.existence_ivl_initial_time local.mem_existence_ivl_iv_defined(1)
local.mem_existence_ivl_iv_defined(2) mem_is_interval_1_I mvar.interval)
subgoal
apply (rule imageI)
by (simp add: vec1_of_flow1_def flow1_of_vec1_def)
done
done
theorem einterpret_solve_poincare_fas:
assumes wd: "wd TYPE('n rvec)"
assumes "length CXs = D + D*D" "n < D"
assumes nz: "ode (fst (eucl_of_list CXs::'n vec1)) ∙ Basis_list ! n ≠ 0"
shows
"flow1_of_vec1 (einterpret (solve_poincare_fas n) CXs::'n::enum vec1) =
(let (x, d) = flow1_of_vec1 (eucl_of_list CXs::'n vec1) in (x,
d - (blinfun_scaleR_left (ode (x)) o⇩L
(blinfun_scaleR_left (inverse (ode x ∙ Basis_list ! n)) o⇩L (blinfun_inner_left (Basis_list ! n) o⇩L d)))))"
using assms
apply (auto intro!: simp: flow1_of_vec1_def solve_poincare_fas_def)
subgoal
apply (auto intro!: euclidean_eqI[where 'a="'n rvec"])
apply (subst eucl_of_list_prod)
by (auto simp: eucl_of_list_prod length_concat o_def sum_list_distinct_conv_sum_set D_def Let_def
wdD[OF wd] take_eq_map_nth)
subgoal premises prems
proof -
have ode_e_eq: "interpret_floatarith (ode_e ! i) (map ((!) CXs) [0..<CARD('n)]) = interpret_floatarith (ode_e ! i) CXs"
if "i < D"
for i
apply (rule interpret_floatarith_max_Var_cong)
apply (drule max_Var_floatariths_lessI)
using that apply (simp add: wdD[OF wd])
apply (subst nth_map)
apply auto
using wdD[OF wd]
apply simp
using wdD[OF wd]
apply simp
done
define z where "z = (0::float)"
show ?thesis
supply [simp] = snd_eucl_of_list_prod fst_eucl_of_list_prod
supply [simp del] = eucl_of_list_take_DIM
using prems unfolding z_def[symmetric] D_def Let_def
including blinfun.lifting
apply (transfer fixing: CXs n z)
unfolding z_def
apply (auto simp: o_def ode_def intro!: ext)
apply (vector matrix_vector_mult_def )
apply (auto intro!: blinfun_euclidean_eqI simp: inner_Basis_eq_vec_nth wdD[OF wd])
apply (auto simp: length_concat o_def sum_list_distinct_conv_sum_set wdD[OF wd] take_eq_map_nth)
apply (auto simp: concat_map_map_index)
apply (vector )
apply (subst vec_nth_eq_list_of_eucl2 vec_nth_eq_list_of_eucl1)+
apply (subst (asm) vec_nth_eq_list_of_eucl2 vec_nth_eq_list_of_eucl1)+
apply (simp add: less_imp_le wdD[OF wd] index_nth_id )
apply (auto simp: algebra_simps ode_e_eq wdD[OF wd] divide_simps)
done
qed
done
lemma choose_step'_flowpipe:
assumes wd[refine_vcg]: "wd TYPE('n::enum rvec)"
assumes safe: "fst ` X0 ⊆ Csafe"
shows "var.choose_step (X0::'n vec1 set) h ≤ SPEC (λ(h', _, RES_ivl, RES::'n vec1 set).
0 < h' ∧ h' ≤ h ∧ flowpipe (flow1_of_vec1 ` X0) h' h' (flow1_of_vec1 ` RES_ivl) (flow1_of_vec1 ` RES))"
apply refine_vcg
apply auto
apply (frule var.flowpipe0_safeD)
apply (drule var_flowpipe0_flowpipe[rotated])
by (auto simp: safe_eq wd)
lemma max_Var_floatariths_solve_poincare_fas[le]:
assumes wd: "wd (TYPE('n::enum rvec))"
shows "i < D ⟹ max_Var_floatariths (solve_poincare_fas i) ≤ D + D * D"
by (auto simp: solve_poincare_fas_def concat_map_map_index Let_def
intro!: max_Var_floatariths_leI Suc_leI)
(auto intro!: max_Var_floatarith_le_max_Var_floatariths_nthI max_Var_floatariths_ode_e_wd[OF wd]
simp: wdD[OF wd])
lemma length_solve_poincare_fas[simp]: "length (solve_poincare_fas n) = D + D * D"
by (auto simp: solve_poincare_fas_def length_concat o_def sum_list_distinct_conv_sum_set D_def Let_def)
theorem interpret_floatariths_solve_poincare_fas:
assumes wd: "wd TYPE('n::enum rvec)"
assumes "length CXs = D + D*D" "n < D"
assumes nz: "ode (fst (eucl_of_list CXs::'n vec1)) ∙ Basis_list ! n ≠ 0"
shows
"interpret_floatariths (solve_poincare_fas n) CXs =
list_of_eucl (vec1_of_flow1 (let (x, d) = flow1_of_vec1 (eucl_of_list CXs::'n vec1) in (x,
d - (blinfun_scaleR_left (ode (x)) o⇩L
(blinfun_scaleR_left (inverse (ode x ∙ Basis_list ! n)) o⇩L (blinfun_inner_left (Basis_list ! n) o⇩L d))))))"
using arg_cong[where f="list_of_eucl::'n vec1 ⇒ _", OF arg_cong[where f=vec1_of_flow1, OF einterpret_solve_poincare_fas[OF assms]]]
apply auto
apply (subst (asm) list_of_eucl_eucl_of_list)
apply auto
apply (auto simp: wdD[OF wd])
done
lemma length_solve_poincare_slp[simp]: "length solve_poincare_slp = D"
by (auto simp: solve_poincare_slp_def)
lemma ne_zero_lemma:
assumes
"ode ` fst ` CX ⊆ FC"
"∀b∈FC. b ∙ n ≠ 0"
"(a, b) ∈ CX"
"ode a ∙ n = 0"
shows "False"
proof -
have "(a, b) ∈ CX" by fact
then have "ode (fst (a, b)) ∈ ode ` fst ` CX" by blast
also have "… ⊆ FC"
by fact
finally have "ode a ∈ FC" by simp
with assms show False
by auto
qed
lemma ne_zero_lemma2:
assumes
"ode ` fst ` flow1_of_vec1 ` env ⊆ F"
"∀x∈F. x ∙ n ≠ 0"
"(a, b) ∈ env"
"flow1_of_vec1 (a, b) = (a', b')"
"ode a' ∙ n = 0"
shows False
proof -
have "(a', b') ∈ flow1_of_vec1 ` env"
apply (rule image_eqI)
using assms by auto
then have "ode (fst (a', b')) ∈ ode ` fst ` …" by blast
also from assms have "… ⊆ F" by simp
finally have "ode a' ∈ F" by simp
with assms have "ode a' ∙ n ≠ 0" by auto
with assms show False by simp
qed
lemma solve_poincare_plane[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
assumes "n ∈ Basis"
shows "solve_poincare_plane (n::'n::enum rvec) CX ≤ SPEC (λPDP.
fst ` PDP ⊆ Csafe ∧
(∀(x, d) ∈ CX. (x, d - (blinfun_scaleR_left (ode x) o⇩L
(blinfun_scaleR_left (inverse (ode x ∙ n)) o⇩L (blinfun_inner_left n o⇩L d)))) ∈ PDP) ∧
(∀(x, d) ∈ PDP. ode x ∙ n ≠ 0))"
unfolding solve_poincare_plane_def
apply (refine_vcg)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by (auto simp: solve_poincare_slp_def)
subgoal using assms by auto
subgoal for C1 FC _ CX' CX'' P P1 FP _
apply auto
apply (drule bspec, assumption)
apply (rule image_eqI)
prefer 2 apply assumption
apply (subst einterpret_solve_poincare_fas)
subgoal using wd by auto
subgoal using wd by auto
subgoal using wd by auto
subgoal using wd assms by (auto elim!: ne_zero_lemma)
subgoal using wd assms by auto
done
subgoal by (auto elim!: ne_zero_lemma2)
done
lemma choose_step1_flowpipe[le, refine_vcg]:
assumes wd[refine_vcg]: "wd TYPE('n::enum rvec)"
shows "choose_step1 (X0::'n eucl1 set) h ≤ SPEC (λ(h', _, RES_ivl, RES::'n eucl1 set).
0 < h' ∧ h' ≤ h ∧ flowpipe X0 h' h' RES_ivl RES)"
using assms
unfolding choose_step1_def
by (refine_vcg choose_step'_flowpipe[le] wd)
(auto simp: image_image,
auto simp: safe_eq vec1_of_flow1_def flowpipe0_imp_flowpipe env_len_def)
lemma image_flow1_of_vec1I:
"vec1_of_flow1 x ∈ X ⟹ x ∈ flow1_of_vec1 ` X"
by (rule image_eqI) (rule flow1_of_vec1_vec1_of_flow1[symmetric])
lemma inter_sctn1_spec[le, refine_vcg]:
"inter_sctn1_spec X sctn ≤ SPEC (λ(R, S). X ∩ plane_of sctn × UNIV ⊆ R ∧ fst ` R ⊆ plane_of sctn
∧ X ∩ plane_of sctn × UNIV ⊆ S ∧ fst ` S ⊆ plane_of sctn)"
unfolding inter_sctn1_spec_def
apply (refine_vcg, auto)
subgoal by (rule image_flow1_of_vec1I) (auto simp: plane_of_def inner_prod_def)
subgoal by (auto simp: plane_of_def inner_prod_def)
subgoal by (rule image_flow1_of_vec1I)
(force simp: set_plus_def plane_of_def inner_prod_def vec1_of_flow1_def)
subgoal by (force simp: set_plus_def)
done
lemma fst_safe_coll[le, refine_vcg]:
"wd TYPE('a) ⟹
fst_safe_coll (X::('a::executable_euclidean_space*'c) set) ≤ SPEC (λR. R = fst ` X ∧ fst ` X ⊆ Csafe)"
unfolding fst_safe_coll_def
by refine_vcg
lemma vec1reps[THEN order_trans, refine_vcg]: "vec1reps CX ≤ SPEC (λR. case R of None ⇒ True | Some X ⇒ X = vec1_of_flow1 ` CX)"
unfolding vec1reps_def
apply (refine_vcg FORWEAK_mono_rule[where
I="λXS R. case R of None ⇒ True | Some R ⇒ vec1_of_flow1 ` (⋃XS) ⊆ R ∧ R ⊆ vec1_of_flow1 ` CX"])
by (auto simp: split: option.splits) force+
lemma nonzero_component_within[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "nonzero_component_within ivl sctn (PDP::'n eucl1 set) ≤ SPEC (λb.
(b ⟶ (∀x∈PDP. fst x ∈ ivl ∧ (∀⇩F x in at (fst x) within plane_of sctn. x ∈ ivl))) ∧
fst ` PDP ⊆ Csafe ∧
(∀x∈PDP. ode (fst x) ∙ normal sctn ≠ 0))"
unfolding nonzero_component_within_def
by refine_vcg auto
lemma do_intersection_invar_inside:
"do_intersection_invar guards b ivl sctn X (e, f, m, n, p, q, True) ⟹
fst ` e ⊆ sabove_halfspace sctn ⟹
fst ` mn ⊆ ivl ⟹
mn = m ∨ mn = n ⟹
do_intersection_spec UNIV guards ivl sctn X (mn, p)"
subgoal premises prems
proof -
from prems have e: "e ∩ sbelow_halfspace sctn × UNIV = {}"
by (auto simp: halfspace_simps plane_of_def)
with prems(1) have
"poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} X UNIV p m"
"poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} X UNIV p n"
"e ∩ sbelow_halfspace sctn × UNIV = {}"
"fst ` X ∩ b = {}"
"fst ` X ⊆ sbelow_halfspace sctn"
"ivl ⊆ plane (normal sctn) (pstn sctn)"
"fst ` X ⊆ p"
"fst ` m ⊆ Csafe"
"fst ` n ⊆ Csafe"
"p ⊆ Csafe"
"fst ` e ⊆ Csafe"
"f ⊆ {0..}"
"p ⊆ sbelow_halfspace sctn - guards"
"e ⊆ (- guards) × UNIV"
"fst ` (m ∪ n) ∩ guards = {}"
"0 ∉ (λx. ode x ∙ normal sctn) ` fst ` (m ∪ n)"
"∀x∈m ∪ n. ∀⇩F x in at (fst x) within plane (normal sctn) (pstn sctn). x ∈ ivl"
by (auto simp: do_intersection_invar_def do_intersection_spec_def plane_of_def)
then show ?thesis
using prems(2-)
by (auto simp: do_intersection_spec_def plane_of_def halfspace_simps)
qed
done
lemma do_intersection_body_lemma:
assumes "flowsto A T (i × UNIV) (X' ∩ sbelow_halfspace sctn × UNIV)"
"poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} B UNIV i PS "
"poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} B UNIV i PS2"
"T ⊆ {0..}"
"i ⊆ sbelow_halfspace sctn - guards"
"fst ` (A ∪ B) ⊆ sbelow_halfspace sctn"
"fst ` PS ⊆ Csafe "
"fst ` PS2 ⊆ Csafe "
‹X = A ∪ B›
assumes ivl: "closed ivl" "ivl ⊆ plane_of sctn"
assumes normal_Basis: "¦normal sctn¦ ∈ Basis"
and inter_empties: "fst ` Y ∩ GUARDS = {}" "fst ` CX' ∩ GUARDS = {}"
"fst ` PDP' ∩ GUARDS = {}" "fst ` PDP'' ∩ GUARDS = {}"
and h': "0 < h'" "h' ≤ h"
and safe: "fst ` PDP ⊆ Csafe" "fst ` CX' ⊆ Csafe"
"fst ` PDP' ⊆ Csafe"
"fst ` PDP'' ⊆ Csafe"
and PDP:
"∀(x,d)∈CX'. (x,
d - (blinfun_scaleR_left (ode x) o⇩L
(blinfun_scaleR_left (inverse (ode x ∙ ¦normal sctn¦)) o⇩L
(blinfun_inner_left ¦normal sctn¦ o⇩L d))))
∈ PDP"
and PDP': "PDP ∩ plane_of sctn × UNIV ⊆ PDP'"
and PDP'': "PDP ∩ plane_of sctn × UNIV ⊆ PDP''"
and evin:
"∀x∈PDP'. fst x ∈ ivl ∧ (∀⇩F x in at (fst x) within plane_of sctn. x ∈ ivl)"
"∀x∈PDP''. fst x ∈ ivl ∧ (∀⇩F x in at (fst x) within plane_of sctn. x ∈ ivl)"
and through: "∀(x, d)∈PDP. ode x ∙ ¦normal sctn¦ ≠ 0"
"∀x∈PDP'. ode (fst x) ∙ normal sctn ≠ 0"
"∀x∈PDP''. ode (fst x) ∙ normal sctn ≠ 0"
and plane:
"fst ` PDP' ⊆ plane_of sctn"
"fst ` PDP'' ⊆ plane_of sctn"
and flowpipe: "flowpipe X' h' h' CX' Y"
shows "∃A B. X = A ∪ B ∧
flowsto A {0<..} ((fst ` CX' ∩ sbelow_halfspace sctn ∪ i) × UNIV) (Y ∩ sbelow_halfspace sctn × UNIV) ∧
poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} B UNIV (fst ` CX' ∩ sbelow_halfspace sctn ∪ i) (PDP' ∪ PS) ∧
poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} B UNIV (fst ` CX' ∩ sbelow_halfspace sctn ∪ i) (PDP'' ∪ PS2)"
proof -
from flowpipe
have 1: "flowpipe (X' ∩ (sbelow_halfspace sctn) × UNIV) h' h' CX' Y"
by (rule flowpipe_subset) (use flowpipe in ‹auto dest!: flowpipe_safeD›)
have 2: "fst ` (X' ∩ (sbelow_halfspace sctn) × UNIV) ∩ {x. pstn sctn ≤ x ∙ normal sctn} = {}"
by (auto simp: halfspace_simps plane_of_def)
from normal_Basis have 3: "normal sctn ≠ 0"
by auto
note 4 = ‹closed ivl›
from ‹ivl ⊆ plane_of sctn› have 5: "ivl ⊆ plane (normal sctn) (pstn sctn)"
by (auto simp: plane_of_def)
have 6: "(x, d) ∈ CX' ⟹ x ∈ plane (normal sctn) (pstn sctn) ⟹
(x, d - (blinfun_scaleR_left (ode x) o⇩L
(blinfun_scaleR_left (inverse (ode x ∙ normal sctn)) o⇩L (blinfun_inner_left (normal sctn) o⇩L d))))
∈ PDP' ∩ PDP''" for x d
unfolding PDP_abs_lemma[OF normal_Basis]
apply (drule PDP[rule_format, of "(x, d)", unfolded split_beta' fst_conv snd_conv])
using PDP' PDP''
by (auto simp: plane_of_def)
from normal_Basis through
have 7: "(x, d) ∈ PDP' ⟹ ode x ∙ normal sctn ≠ 0" for x d
by (auto elim!: abs_in_BasisE)
have 8: "(x, d) ∈ PDP' ⟹ x ∈ ivl" for x d
using evin by auto
have 9: "(x, d) ∈ PDP' ⟹ ∀⇩F x in at x within plane (normal sctn) (pstn sctn). x ∈ ivl" for x d
using evin by (auto simp add: plane_of_def)
obtain X1 X2
where X1X2: "X' ∩ sbelow_halfspace sctn × UNIV = X1 ∪ X2"
and X1: "flowsto X1 {0<..h'} (CX' ∩ {x. x ∙ normal sctn < pstn sctn} × UNIV)
(CX' ∩ {x ∈ ivl. x ∙ normal sctn = pstn sctn} × UNIV)"
and X2: "flowsto X2 {h'..h'} (CX' ∩ {x. x ∙ normal sctn < pstn sctn} × UNIV)
(Y ∩ {x. x ∙ normal sctn < pstn sctn} × UNIV)"
and P: "poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} X1 UNIV
(fst ` CX' ∩ {x. x ∙ normal sctn < pstn sctn}) (PDP' ∩ PDP'')"
by (rule flowpipe_split_at_above_halfspace[OF 1 2 3 4 5 6 7 8 9]) (auto simp: Ball_def)
from ‹flowsto A _ _ _›[unfolded X1X2]
obtain p1 p2 where p1p2: "A = p1 ∪ p2" and p1: "flowsto p1 T (i × UNIV) X1" and p2: "flowsto p2 T (i × UNIV) X2"
by (rule flowsto_unionE)
have "A ∪ B = p2 ∪ (p1 ∪ B)" using ‹A = p1 ∪ p2›
by auto
moreover
from flowsto_trans[OF p2 X2]
have "flowsto p2 {0<..} ((fst ` CX' ∩ (sbelow_halfspace sctn) ∪ i) × UNIV)
(Y ∩ (sbelow_halfspace sctn) × UNIV)"
apply (rule flowsto_subset)
subgoal by (auto simp: halfspace_simps)
subgoal using h' ‹T ⊆ _› by (auto simp: halfspace_simps intro!: add_nonneg_pos)
subgoal
using flowpipe_source_subset[OF 1, unfolded X1X2] X1X2
apply auto
by (auto simp: halfspace_simps)
subgoal by (auto simp: halfspace_simps)
done
moreover
have cls: "closed {x ∈ ivl. x ∙ normal sctn = pstn sctn}"
by (rule closed_levelset_within continuous_intros ‹closed ivl›)+
from flowsto_trans[OF p1 X1]
have ftt: "flowsto p1 ({s + t |s t. s ∈ T ∧ t ∈ {0<..h'}})
(i × UNIV ∪ CX' ∩ {x. x ∙ normal sctn < pstn sctn} × UNIV ∪ X1 ∩ X1)
(X1 - X1 ∪ CX' ∩ {x ∈ ivl. x ∙ normal sctn = pstn sctn} × UNIV)"
by auto
from X1X2 have X1_sb: "X1 ⊆ sbelow_halfspace sctn × UNIV" by auto
have "{x ∈ ivl. x ∙ normal sctn = pstn sctn} × UNIV ∩ (i × UNIV ∪ CX' ∩ {x. x ∙ normal sctn < pstn sctn} × UNIV ∪ X1) = {}"
apply (intro Int_Un_eq_emptyI)
subgoal using ‹i ⊆ sbelow_halfspace sctn - guards› by (auto simp: halfspace_simps)
subgoal by (auto simp: halfspace_simps)
subgoal using X1_sb by (auto simp: halfspace_simps)
done
then have inter_empty:
"{x ∈ ivl. x ∙ normal sctn = pstn sctn} × UNIV ∩ (i × UNIV ∪ CX' ∩ {x. x ∙ normal sctn < pstn sctn} × UNIV ∪ X1 ∩ X1) = {}"
by auto
have p1ret: "returns_to {x ∈ ivl. x ∙ normal sctn = pstn sctn} x"
and p1pm: "poincare_map {x ∈ ivl. x ∙ normal sctn = pstn sctn} x ∈ fst ` (PDP' ∩ PDP'')"
if "(x, d) ∈ p1" for x d
apply (rule flowsto_poincareD[OF ftt _ inter_empty _ _ _ order_refl])
subgoal by auto
subgoal by fact
subgoal using ‹T ⊆ _› by auto
subgoal using that by auto
subgoal
apply (rule flowsto_poincareD[OF ftt _ inter_empty])
subgoal by auto
subgoal by fact
subgoal using ‹T ⊆ _› by auto
subgoal using that by auto
subgoal using 6 by force
done
done
have crt: "isCont (return_time {x ∈ ivl. x ∙ normal sctn - pstn sctn = 0}) x" if "(x, d) ∈ p1" for x d
apply (rule return_time_isCont_outside[where Ds="λ_. blinfun_inner_left (normal sctn)"])
subgoal by (simp add: p1ret[OF that])
subgoal by fact
subgoal by (auto intro!: derivative_eq_intros)
subgoal by simp
subgoal apply simp
using p1pm[OF that]
by (auto dest!: 7)
subgoal
using p1pm[OF that]
by (auto dest!: 9 simp: eventually_at_filter)
subgoal
using ‹fst ` (A ∪ B) ⊆ sbelow_halfspace sctn› that p1p2
by (auto simp: halfspace_simps)
done
have pmij: "poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} p1 UNIV
(fst ` (i × UNIV ∪ X1) ∪ fst ` CX' ∩ {x. x ∙ normal sctn < pstn sctn}) (PDP' ∩ PDP'')"
apply (rule flowsto_poincare_trans[OF ‹flowsto _ _ _ X1› P])
subgoal using ‹T ⊆ {0..}› by auto
subgoal by auto
subgoal
using ‹i ⊆ sbelow_halfspace sctn - guards› X1X2
by (force simp: halfspace_simps)
subgoal by fact
subgoal for x d using crt by simp
subgoal by auto
done
from pmij have "poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} p1 UNIV (fst ` (i × UNIV ∪ X1) ∪ fst ` CX' ∩ {x. x ∙ normal sctn < pstn sctn}) PDP'"
apply (rule poincare_mapsto_subset)
using ‹fst ` PDP' ⊆ Csafe›
by auto
from this ‹poincare_mapsto _ _ _ i PS›
have "poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} (p1 ∪ B) UNIV
((fst ` (i × UNIV ∪ X1) ∪ fst ` CX' ∩ {x. x ∙ normal sctn < pstn sctn}) ∪ i) (PDP' ∪ PS)"
by (intro poincare_mapsto_unionI) (auto simp: plane_of_def)
then have "poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} (p1 ∪ B) UNIV (fst ` CX' ∩ sbelow_halfspace sctn ∪ i) (PDP' ∪ PS)"
apply (rule poincare_mapsto_subset)
subgoal by auto
subgoal by auto
subgoal
using flowpipe_source_subset[OF 1, unfolded X1X2] X1X2
apply (auto simp: halfspace_simps subset_iff)
done
subgoal using safe ‹fst ` PS ⊆ Csafe› by auto
done
moreover
from pmij have "poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} p1 UNIV (fst ` (i × UNIV ∪ X1) ∪ fst ` CX' ∩ {x. x ∙ normal sctn < pstn sctn}) PDP''"
apply (rule poincare_mapsto_subset)
using ‹fst ` PDP'' ⊆ Csafe›
by auto
from this ‹poincare_mapsto _ _ _ i PS2›
have "poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} (p1 ∪ B) UNIV
((fst ` (i × UNIV ∪ X1) ∪ fst ` CX' ∩ {x. x ∙ normal sctn < pstn sctn}) ∪ i) (PDP'' ∪ PS2)"
by (intro poincare_mapsto_unionI) (auto simp: plane_of_def)
then have "poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} (p1 ∪ B) UNIV (fst ` CX' ∩ sbelow_halfspace sctn ∪ i) (PDP'' ∪ PS2)"
apply (rule poincare_mapsto_subset)
subgoal by auto
subgoal by auto
subgoal
using flowpipe_source_subset[OF 1, unfolded X1X2] X1X2
apply (auto simp: halfspace_simps subset_iff)
done
subgoal using safe ‹fst ` PS2 ⊆ Csafe› by auto
done
ultimately
show ?thesis
unfolding ‹X = A ∪ B› by blast
qed
lemma do_intersection_body_spec:
fixes guards::"'n::enum rvec set"
assumes invar: "do_intersection_invar guards GUARDS ivl sctn X (X', T, PS, PS2, i, True, True)"
and wdp[refine_vcg]: "wd TYPE('n rvec)"
and X: "fst ` X ⊆ Csafe"
and ivl: "closed ivl" and GUARDS: "guards ⊆ GUARDS"
shows "do_intersection_body GUARDS ivl sctn h (X', T, PS, PS2, i, True, True) ≤
SPEC (do_intersection_invar guards GUARDS ivl sctn X)"
proof -
from invar
obtain A B where AB: "fst ` (A ∪ B) ∩ GUARDS = {} "
"fst ` (A ∪ B) ⊆ sbelow_halfspace sctn "
"ivl ⊆ plane_of sctn "
"fst ` (A ∪ B) ⊆ i "
"fst ` PS ⊆ Csafe "
"fst ` PS2 ⊆ Csafe "
"i ⊆ Csafe "
"fst ` X' ⊆ Csafe "
"T ⊆ {0..}"
"i ⊆ sbelow_halfspace sctn - guards "
"X' ⊆ (- guards) × UNIV "
"fst ` (PS ∪ PS2) ∩ guards = {} "
"0 ∉ (λx. ode x ∙ normal sctn) ` fst ` (PS ∪ PS2) "
"∀x∈PS ∪ PS2. ∀⇩F x in at (fst x) within plane_of sctn. x ∈ ivl "
"X = A ∪ B "
"flowsto A T (i × UNIV) (X' ∩ sbelow_halfspace sctn × UNIV)"
"poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} B UNIV i PS "
"poincare_mapsto {x ∈ ivl. x ∙ normal sctn = pstn sctn} B UNIV i PS2"
by (auto simp: do_intersection_invar_def)
have ev_in_ivl: "∀⇩F x in at p within plane_of sctn. x ∈ ivl" if
‹∀x∈d. fst x ∈ ivl ∧ (∀⇩F x in at (fst x) within plane_of sctn. x ∈ ivl)›
‹∀x∈e. fst x ∈ ivl ∧ (∀⇩F x in at (fst x) within plane_of sctn. x ∈ ivl)›
‹(p, q) ∈ d ∨ (p, q) ∈ PS ∨ (p, q) ∈ e ∨ (p, q) ∈ PS2›
for p q d e
using ‹∀x∈PS ∪ PS2. ∀⇩F x in at (fst x) within plane_of sctn. x ∈ ivl›
using that
by (auto dest!: bspec[where x="(p, q)"])
show ?thesis
unfolding do_intersection_body_def do_intersection_invar_def
apply simp
apply (refine_vcg, clarsimp_all)
subgoal using AB by auto
subgoal using AB by auto
subgoal using AB by auto
subgoal
apply (rule conjI)
subgoal using AB by auto
subgoal using AB by fastforce
done
subgoal using AB by auto
subgoal using AB by auto
subgoal using AB by auto
subgoal by (auto dest!: flowpipe_safeD)
subgoal
apply safe
subgoal using AB GUARDS by auto
subgoal using AB by auto
subgoal using AB by auto
subgoal using AB GUARDS by auto
subgoal using AB by auto
subgoal using AB by auto
done
subgoal using AB GUARDS by auto
subgoal using AB GUARDS by auto
subgoal using AB GUARDS by auto
subgoal using AB assms by (auto intro: ev_in_ivl)
subgoal using AB assms apply - by (rule do_intersection_body_lemma)
done
qed
lemma
do_intersection_spec[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "do_intersection guards ivl sctn (X::'n eucl1 set) h ≤
SPEC (λ(inside, P, P2, CX). (inside ⟶
(do_intersection_spec UNIV guards ivl sctn X (P, CX) ∧
do_intersection_spec UNIV guards ivl sctn X (P2, CX)) ∧ fst ` X ⊆ CX))"
using assms
unfolding do_intersection_def autoref_tag_defs
apply (refine_vcg, clarsimp_all)
subgoal
unfolding do_intersection_invar_def
apply clarsimp
apply (intro conjI)
apply force
apply force
apply force
apply (rule exI[where x=X])
apply (rule exI[where x="{}"])
by (auto intro!: flowsto_self)
subgoal by (rule do_intersection_body_spec)
subgoal by (rule do_intersection_invar_inside, assumption) auto
subgoal by (rule do_intersection_invar_inside, assumption) auto
subgoal by (auto simp: plane_of_def halfspace_simps do_intersection_invar_def)
done
lemma mem_flow1_of_vec1_image_iff[simp]:
"(c, d) ∈ flow1_of_vec1 ` a ⟷ vec1_of_flow1 (c, d) ∈ a"
by force
lemma mem_vec1_of_flow1_image_iff[simp]:
"(c, d) ∈ vec1_of_flow1 ` a ⟷ flow1_of_vec1 (c, d) ∈ a"
by force
lemma split_spec_param1[le, refine_vcg]: "split_spec_param1 X ≤ SPEC (λ(A, B). X ⊆ A ∪ B)"
unfolding split_spec_param1_def
apply (refine_vcg)
apply (auto simp add: subset_iff split: option.splits)
by (metis flow1_of_vec1_vec1_of_flow1 surjective_pairing)
lemma do_intersection_spec_empty:
"X = {} ⟹ Y = {} ⟹ do_intersection_spec S sctns ivl sctn X ({}, Y)"
by (auto simp: do_intersection_spec_def halfspaces_union)
lemma do_intersection_spec_subset:
"do_intersection_spec S osctns ivl csctns Y (a, b) ⟹ X ⊆ Y ⟹ do_intersection_spec S osctns ivl csctns X (a, b)"
by (auto simp: do_intersection_spec_def halfspaces_union intro: flowsto_subset poincare_mapsto_subset)
lemma do_intersection_spec_union:
"do_intersection_spec S osctns ivl csctns a (b, c) ⟹
do_intersection_spec S osctns ivl csctns f (g, h) ⟹
do_intersection_spec S osctns ivl csctns (a ∪ f) (b ∪ g, c ∪ h)"
by (auto simp: do_intersection_spec_def intro!: poincare_mapsto_unionI)
lemma scaleR2_rep_of_coll[le, refine_vcg]:
"scaleR2_rep_coll X ≤ SPEC (λ((l, u), Y). X ⊆ scaleR2 l u Y)"
unfolding scaleR2_rep_coll_def
apply (refine_vcg FORWEAK_mono_rule[where I="λXs ((l, u), Y). ⋃Xs ⊆ scaleR2 l u Y"])
subgoal by (auto intro: scaleR2_subset)
subgoal
apply clarsimp
apply safe
subgoal by (auto elim: scaleR2_subset)
subgoal
apply (rule set_rev_mp, assumption)
apply (rule order_trans)
apply (rule Union_upper, assumption)
apply (rule order_trans, assumption)
apply (rule subsetI)
apply (erule scaleR2_subset)
by (auto )
done
done
lemma split_spec_param1e[le, refine_vcg]: "split_spec_param1e X ≤ SPEC (λ(A, B). X ⊆ A ∪ B)"
unfolding split_spec_param1e_def
apply (refine_vcg)
apply clarsimp
apply (thin_tac "_ ≠ {}")
apply (auto simp: scaleR2_def vimage_def image_def)
apply (rule exI, rule conjI, assumption, rule conjI, assumption)
apply (auto simp: split_beta')
apply (drule_tac x = x in spec)
apply auto
by (metis (no_types, lifting) UnE prod.sel(1) prod.sel(2) subset_eq)
lemma reduce_spec1[le, refine_vcg]: "reduce_spec1 ro X ≤ SPEC (λR. X ⊆ R)"
unfolding reduce_spec1_def
by refine_vcg auto
lemma reduce_spec1e[le, refine_vcg]: "reduce_spec1e ro X ≤ SPEC (λR. X ⊆ R)"
unfolding reduce_spec1e_def
by refine_vcg (auto simp: scaleR2_def image_def vimage_def, force)
lemma split_under_threshold[le, refine_vcg]:
"split_under_threshold ro th X ≤ SPEC (λR. X ⊆ R)"
unfolding split_under_threshold_def autoref_tag_defs
by (refine_vcg) auto
lemma step_split[le, refine_vcg]:
"wd TYPE((real, 'n::enum) vec) ⟹ step_split ro (X::'n eucl1 set) ≤ SPEC (λY. X ⊆ Y ∧ fst ` Y ⊆ Csafe)"
unfolding step_split_def
by (refine_vcg refine_vcg) auto
lemma tolerate_error_SPEC[THEN order_trans, refine_vcg]:
"tolerate_error Y E ≤ SPEC (λb. True)"
unfolding tolerate_error_def
by refine_vcg
lemma flowpipe_scaleR2I: "flowpipe (scaleR2 x1 x2 bc) x1a x1a (fst ` aca × UNIV) (scaleR2 x1 x2 bca)"
if "flowpipe (bc) x1a x1a (fst ` aca × UNIV) (bca)"
using that
apply (auto simp: flowpipe_def scaleR2_def)
apply (drule bspec, assumption)
apply (auto simp: image_def vimage_def )
apply (rule exI, rule conjI, assumption, rule conjI, assumption)
apply (rule bexI) prefer 2 apply assumption
by (auto simp: scaleR_blinfun_compose_right)
lemma choose_step1e_flowpipe[le, refine_vcg]:
assumes vwd[refine_vcg]: "wd TYPE('n::enum rvec)"
shows "choose_step1e (X0::'n eucl1 set) h ≤ SPEC (λ(h', _, RES_ivl, RES::'n eucl1 set).
0 < h' ∧ h' ≤ h ∧ flowpipe X0 h' h' (RES_ivl × UNIV) RES)"
unfolding choose_step1e_def
apply (refine_vcg)
apply (auto intro: flowpipe_scaleR2I)
apply (erule contrapos_np)
apply (auto intro!: flowpipe_scaleR2I)
apply (rule flowpipe_subset)
apply assumption
apply (auto dest!: flowpipe_safeD)
done
lemma width_spec_appr1[THEN order_trans, refine_vcg]: "width_spec_appr1 X ≤ SPEC (λ_. True)"
unfolding width_spec_appr1_def
by refine_vcg
lemma tolerate_error1_SPEC[THEN order_trans, refine_vcg]:
"tolerate_error1 Y E ≤ SPEC (λb. True)"
unfolding tolerate_error1_def
by refine_vcg
lemma
step_adapt_time[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "step_adapt_time (X::'n eucl1 set) h ≤ SPEC (λ(t, CX, X1, h). flowpipe X t t (CX × UNIV) X1)"
unfolding step_adapt_time_def autoref_tag_defs
apply (refine_vcg refine_vcg, clarsimp)
apply (auto simp: flowpipe_def)
apply force
done
lemma
resolve_step[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "resolve_step roptns (X::'n::enum eucl1 set) h ≤ SPEC (λ(_, CX, X1, _).
flowsto X {0..} (CX × UNIV) X1 ∧ X ∪ X1 ⊆ CX × UNIV ∧ X1 ∪ CX × UNIV ⊆ Csafe × UNIV)"
unfolding resolve_step_def autoref_tag_defs
apply (refine_vcg refine_vcg)
subgoal by (rule flowsto_self) auto
subgoal by auto
subgoal by auto
subgoal
apply clarsimp
apply (frule flowpipe_imp_flowsto_nonneg)
apply (rule flowsto_subset, assumption)
by auto
subgoal
by (auto dest: flowpipe_source_subset)
subgoal
by (auto dest!: flowpipe_safeD)
done
lemma pre_intersection_step[THEN order_trans, refine_vcg]:
"pre_intersection_step ro (X::'n eucl1 set) h ≤ SPEC (λ(X', CX, G). X ⊆ X' ∪ G ∧ X ∪ X' ∪ G ⊆ CX × UNIV)"
if [refine_vcg]: "wd TYPE('n::enum rvec)"
unfolding pre_intersection_step_def autoref_tag_defs
by (refine_vcg) auto
lemma [THEN order_trans, refine_vcg]: "select_with_inter ci a ≤ SPEC (λ_. True)"
unfolding select_with_inter_def
by (refine_vcg FORWEAK_mono_rule[where I="λ_ _. True"])
lemmas [refine_vcg del] = scaleR2_rep_of_coll
lemma fst_scaleR2_image[simp]: "ad ≤ ereal r ⟹ ereal r ≤ bd ⟹ fst ` scaleR2 ad bd be = fst ` be"
by (cases ad; cases bd; force simp: scaleR2_def image_image split_beta' vimage_def)
lemma scaleR2_rep_of_coll2[le, refine_vcg]:
"scaleR2_rep_coll X ≤ SPEC (λ((l, u), Y). X ⊆ scaleR2 l u Y ∧ fst ` X = fst ` Y)"
unfolding scaleR2_rep_coll_def
supply [simp del] = mem_scaleR2_union
apply (refine_vcg FORWEAK_mono_rule[where I="λXs ((l, u), Y).
⋃Xs ⊆ scaleR2 l u Y ∧ fst ` ⋃Xs ⊆ fst ` Y ∧ fst ` Y ⊆ fst ` X"])
apply (auto intro: scaleR2_subset)
subgoal by (auto simp: scaleR2_def)
subgoal by (auto simp: scaleR2_def image_def vimage_def, fastforce)
subgoal
apply (rule scaleR2_subset)
apply (rule subsetD)
apply assumption
apply auto
done
subgoal by force
subgoal for a b c d e f g h i j k l
apply (rule scaleR2_subset)
apply (rule subsetD)
apply assumption
by auto
subgoal by (auto simp: scaleR2_def)
subgoal by (auto simp: scaleR2_def)
subgoal by (auto simp: scaleR2_def image_def vimage_def, fastforce)
done
lemma reach_cont[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "reach_cont roptns guards (X::'n eucl1 set) ≤ SPEC (λ(CX, G).
G ∪ (CX × UNIV) ⊆ (Csafe - guards) × UNIV ∧
X ∪ G ⊆ CX × UNIV ∧
flowsto X {0..} (CX × UNIV) G)"
using [[simproc del: defined_all]]
unfolding reach_cont_def autoref_tag_defs
apply (refine_vcg, clarsimp_all simp add: cancel_times_UNIV_subset)
subgoal by (rule flowsto_self) auto
subgoal by (force simp: scaleR2_def)
subgoal by (fastforce simp: scaleR2_def vimage_def image_def)
subgoal premises prems for _ _ _ _ _ _ _ g
using ‹flowsto X _ _ (g ∪ _ ∪ _)› ‹flowsto g _ _ _›
apply (rule flowsto_stepI)
using prems
by auto
subgoal
apply safe
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
subgoal by auto
subgoal
by (rule flowsto_subset, assumption) auto
subgoal
apply safe
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by fastforce
subgoal by auto
subgoal by auto
subgoal
by (metis (mono_tags, lifting) Diff_eq_empty_iff Diff_iff IntI)
done
subgoal
apply safe
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
subgoal by auto
done
lemma reach_cont_par[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "reach_cont_par roptns guards (X::'n eucl1 set) ≤ SPEC (λ(CX, G).
G ∪ (CX × UNIV) ⊆ (Csafe - guards) × UNIV ∧
X ∪ G ⊆ CX × UNIV ∧
flowsto X {0..} (CX × UNIV) G)"
unfolding reach_cont_par_def
apply refine_vcg
apply auto
apply force
apply force
apply force
apply force
subgoal
apply (rule bexI)
prefer 2 apply assumption
by auto
subgoal
apply (rule bexI)
prefer 2 apply assumption
by auto
subgoal for R
apply (rule flowsto_source_Union)
apply (drule bspec, assumption)
apply auto
apply (rule flowsto_subset, assumption)
apply auto
done
done
lemma subset_iplane_coll[THEN order_trans, refine_vcg]:
"subset_iplane_coll x ics ≤ SPEC (λb. b ⟶ x ⊆ ics)"
unfolding subset_iplane_coll_def
apply refine_vcg
subgoal for X icss
by (refine_vcg FORWEAK_mono_rule[where I="λic b. b ⟶ X ⊆ ⋃(icss)"]) auto
done
lemma subsets_iplane_coll[THEN order_trans, refine_vcg]:
"subsets_iplane_coll x ics ≤ SPEC (λb. b ⟶ ⋃x ⊆ ics)"
unfolding subsets_iplane_coll_def
by (refine_vcg FORWEAK_mono_rule[where I="λx b. (b ⟶ ⋃x ⊆ ics)"]) auto
lemma symstart_coll[THEN order_trans, refine_vcg]:
assumes [refine_vcg]: "wd (TYPE('n::enum rvec))"
assumes [le, refine_vcg]:
"⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤ SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
shows "symstart_coll symstart X0 ≤ SPEC (λ(CX, X). flowsto ((X0::'n eucl1 set) - trap × UNIV) {0..} (CX × UNIV) X)"
unfolding symstart_coll_def autoref_tag_defs
apply (refine_vcg FORWEAK_mono_rule[where I="λX (CY, Y). flowsto (⋃X - trap × UNIV) {0..} (CY × UNIV) Y"], clarsimp_all)
subgoal by force
subgoal for a b c d e by (rule flowsto_subset, assumption) auto
subgoal by force
subgoal for a b c d e f g
unfolding Un_Diff
apply (rule flowsto_source_unionI)
subgoal by (rule flowsto_subset, assumption) auto
subgoal by (rule flowsto_subset, assumption) auto
done
done
lemma reach_cont_symstart[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
assumes [le, refine_vcg]: "⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤ SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
shows "reach_cont_symstart roptns symstart guards (X::'n eucl1 set) ≤ SPEC (λ(CX, G).
G ∪ (CX × UNIV) ⊆ (Csafe - guards) × UNIV ∧
X ⊆ CX × UNIV ∧
G ⊆ CX × UNIV ∧
flowsto (X - trap × UNIV) {0..} (CX × UNIV) (G))"
unfolding reach_cont_symstart_def autoref_tag_defs
apply (refine_vcg, clarsimp_all)
subgoal by (auto simp: times_subset_iff)
subgoal by auto
subgoal by auto
subgoal for a b c d e f g
apply (rule flowsto_stepI[OF _ _ order_refl])
apply assumption
by assumption auto
done
lemma reach_conts[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
assumes [refine_vcg]: "⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤ SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) X)"
shows "reach_conts roptns symstart trap guards (X::'n eucl1 set) ≤ SPEC (λ(CX, IGs, X0).
⋃(snd ` IGs) ∪ (CX × UNIV) ⊆ (Csafe - guards) × UNIV ∧
X ⊆ CX × UNIV ∧
⋃(snd ` IGs) ⊆ CX × UNIV ∧
⋃(fst ` IGs) ⊆ guards ∧
X = ⋃(X0 ` (snd ` IGs)) ∧
(∀(I, G) ∈ IGs. flowsto (X0 G - trap × UNIV) {0..} (CX × UNIV) G))"
unfolding reach_conts_def autoref_tag_defs
apply (refine_vcg, clarsimp_all)
subgoal for a b
apply (erule flowsto_Diff_to_Union_funE)
apply (force simp: split_beta')
subgoal for f
apply (rule exI[where x=f])
by (auto simp: split_beta')
done
subgoal by (auto)
subgoal by (auto)
subgoal by (auto)
done
lemma leaves_halfspace[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "leaves_halfspace S (X::'n::enum rvec set) ≤
SPEC (λb. case b of None ⇒ S = UNIV
| Some sctn ⇒
(S = below_halfspace sctn ∧ X ⊆ plane_of sctn ∧ (∀x ∈ X. ode x ∙ normal sctn < 0)))"
unfolding leaves_halfspace_def autoref_tag_defs op_set_to_list_def
apply (refine_vcg, clarsimp_all)
subgoal by (force simp add: halfspace_simps plane_of_def)
done
lemma poincare_start_on[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "poincare_start_on guards sctn (X0::'n eucl1 set) ≤ SPEC (λ(X1S, CX1S).
fst ` (X1S ∪ (CX1S × UNIV)) ⊆ Csafe ∧
fst ` X1S ⊆ sbelow_halfspace sctn ∧
fst ` (X1S ∪ (CX1S × UNIV)) ∩ guards = {} ∧
(X0 ⊆ (CX1S × UNIV)) ∧
(∀(x, d) ∈ CX1S × UNIV. ode x ∙ normal sctn < 0) ∧
flowsto X0 pos_reals ((CX1S × UNIV) ∩ (sbelow_halfspace sctn × UNIV)) X1S)"
unfolding poincare_start_on_def autoref_tag_defs
apply refine_vcg
apply (rule FORWEAK_mono_rule[where I="λX0S (X1S, CX1S).
flowsto (⋃X0S) pos_reals ((CX1S × UNIV) ∩ sbelow_halfspace sctn × UNIV) X1S ∧
fst ` (X1S ∪ (CX1S × UNIV)) ⊆ Csafe ∧
(⋃X0S) ⊆ X0 ∧
(⋃X0S) ⊆ (CX1S × UNIV) ∧
fst ` (X1S ∪ (CX1S × UNIV)) ∩ guards = {} ∧
(∀(x, d) ∈ (CX1S × UNIV). ode x ∙ normal sctn < 0) ∧
fst ` X1S ⊆ sbelow_halfspace sctn"])
subgoal by (refine_vcg)
subgoal for A B
apply (refine_vcg)
subgoal
apply (auto simp: dest!: flowpipe_imp_flowsto)
apply (rule flowsto_subset)
apply (rule flowsto_stays_sbelow[where sctn=sctn])
apply (rule flowsto_subset) apply assumption
apply (rule order_refl)
apply force
apply (rule order_refl)
apply (rule order_refl)
apply (auto simp: halfspace_simps)
apply (rule le_less_trans)
prefer 2 apply assumption
apply (drule bspec)
apply (rule subsetD, assumption)
prefer 2 apply assumption
apply auto
done
subgoal by auto
subgoal by force
subgoal by (auto simp: dest!: flowpipe_source_subset)
subgoal by auto
subgoal
apply (auto simp: halfspace_simps subset_iff)
apply (rule le_less_trans[rotated], assumption)
by fastforce
done
subgoal by (auto intro: flowsto_subset) force
subgoal for a b c d
using assms
apply (refine_vcg, clarsimp_all)
subgoal for e f g h i j k l m n
apply (rule flowsto_source_unionI)
subgoal
apply (drule flowpipe_imp_flowsto, assumption)
apply (rule flowsto_subset[OF flowsto_stays_sbelow[where sctn=sctn] order_refl])
apply (rule flowsto_subset[OF _ order_refl], assumption)
apply force
apply (rule order_refl)
apply (rule order_refl)
apply (auto simp: halfspace_simps)
apply (rule le_less_trans)
prefer 2 apply assumption
apply (drule bspec)
apply (rule subsetD, assumption)
prefer 2 apply assumption
apply auto
done
by (auto intro!: flowsto_source_unionI dest!: flowpipe_imp_flowsto intro: flowsto_subset[OF _ order_refl])
subgoal
apply (auto simp: subset_iff)
apply (auto simp: image_Un)
done
subgoal by auto
subgoal by (auto dest!: flowpipe_source_subset)
subgoal by auto
subgoal
apply (auto simp: halfspace_simps subset_iff)
apply (rule le_less_trans[rotated], assumption)
by fastforce
subgoal by auto
done
subgoal by auto
done
lemma op_inter_fst_coll[le, refine_vcg]: "op_inter_fst_coll X Y ≤ SPEC (λR. R = X ∩ Y × UNIV)"
unfolding op_inter_fst_coll_def
by (refine_vcg FORWEAK_mono_rule[where I="λXs R. ⋃Xs ∩ Y × UNIV ⊆ R ∧ R ⊆ X ∩ Y × UNIV"])
auto
lemma scaleRe_ivl_coll_spec[le, refine_vcg]: "scaleRe_ivl_coll_spec l u X ≤ SPEC (λY. Y = scaleR2 l u X)"
unfolding scaleRe_ivl_coll_spec_def
apply (refine_vcg FORWEAK_mono_rule[where I="λXs R. scaleR2 l u (⋃Xs) ⊆ R ∧ R ⊆ scaleR2 l u X"])
apply (auto simp: intro: scaleR2_subset)
subgoal
by (force simp: intro: scaleR2_subset)
done
lemma do_intersection_spec_scaleR2I:
"do_intersection_spec UNIV sctns ivl sctn (scaleR2 x1 x2 baa) (scaleR2 x1 x2 aca, x1b)"
if "do_intersection_spec UNIV sctns ivl sctn (baa) (aca, x1b)"
using that
by (auto simp: do_intersection_spec_def intro!: poincare_mapsto_scaleR2I)
(auto simp: scaleR2_def image_def vimage_def)
lemma do_intersection_core[refine_vcg, le]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "do_intersection_core sctns ivl sctn (X::'n eucl1 set) ≤
SPEC (λ(P1, P2, CX, X0s).
do_intersection_spec UNIV sctns ivl sctn (X - X0s) (P1, CX) ∧
do_intersection_spec UNIV sctns ivl sctn (X - X0s) (P2, CX)
∧ fst ` (X - X0s) ⊆ CX
∧ X0s ⊆ X)"
unfolding do_intersection_core_def autoref_tag_defs
apply (refine_vcg assms, clarsimp_all)
subgoal by (rule do_intersection_spec_scaleR2I) (auto simp: do_intersection_spec_def intro!: )
subgoal by (rule do_intersection_spec_scaleR2I) (auto simp: do_intersection_spec_def intro!: )
subgoal by (fastforce simp: scaleR2_def)
subgoal by (auto simp: do_intersection_spec_def)
subgoal by (auto simp: do_intersection_spec_def)
done
lemma do_intersection_spec_Union:
"do_intersection_spec S sctns ivl sctn (⋃X) A"
if "⋀x. x ∈ X ⟹ do_intersection_spec S sctns ivl sctn x A"
"X ≠ {}"
using that(2)
unfolding do_intersection_spec_def
apply clarsimp
apply safe
subgoal by (rule poincare_mapsto_Union) (auto simp: do_intersection_spec_def dest!: that(1))
subgoal by (auto simp: do_intersection_spec_def dest!: that(1))
subgoal by (auto simp: do_intersection_spec_def dest!: that(1))
subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
subgoal by (force simp: do_intersection_spec_def dest!: that(1))
subgoal by (auto simp: do_intersection_spec_def dest!: that(1))
subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
done
lemma do_intersection_spec_subset2:
"do_intersection_spec S p ivl sctn X1 (ab, CY) ⟹ CY ⊆ CX ⟹ CX ⊆ Csafe ⟹
CX ∩ p = {} ⟹ CX ∩ ivl ∩ plane_of sctn = {} ⟹ X0 ⊆ X1 ⟹
do_intersection_spec S p ivl sctn X0 (ab, CX)"
by (auto simp: do_intersection_spec_def intro: poincare_mapsto_subset)
lemma do_intersection_spec_Union3:
"do_intersection_spec S osctns ivl csctns (⋃x∈X. a x) ((⋃x∈X. b x), (⋃x∈X. c x))"
if "finite X" "X ≠ {}" "⋀x. x ∈ X ⟹ do_intersection_spec S osctns ivl csctns (a x) (b x, c x)"
using that
proof induction
case empty
then show ?case by auto
next
case (insert x F)
show ?case
apply (cases "F = {}")
subgoal using insert by simp
subgoal
apply simp
apply (rule do_intersection_spec_union)
apply (rule insert.prems) apply simp
apply (rule insert.IH)
apply (assumption)
apply (rule insert.prems) apply simp
done
done
qed
lemma do_intersection_coll[le]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "do_intersection_coll sctns ivl sctn (X::'n eucl1 set) ≤
SPEC (λ(P1, P2, CX, X0s).
do_intersection_spec UNIV sctns ivl sctn (X - X0s) (P1, CX) ∧
do_intersection_spec UNIV sctns ivl sctn (X - X0s) (P2, CX)
∧ fst ` (X - X0s) ⊆ CX
∧ X0s ⊆ X)"
unfolding do_intersection_coll_def autoref_tag_defs
apply (refine_vcg, clarsimp_all)
subgoal
apply (rule do_intersection_spec_subset[OF _ diff_subset])
apply (rule do_intersection_spec_Union3)
subgoal by auto
subgoal by auto
subgoal by auto
done
subgoal
apply (rule do_intersection_spec_subset[OF _ diff_subset])
apply (rule do_intersection_spec_Union3)
subgoal by auto
subgoal by auto
subgoal by auto
done
subgoal by fastforce
subgoal by fastforce
done
lemma
do_intersection_flowsto_trans_outside:
assumes "flowsto XS0 {0..} (CX × UNIV) X1"
assumes "do_intersection_spec UNIV guards ivl sctn X1 (P, CP)"
assumes "fst ` X1 ⊆ CP"
assumes "{x ∈ ivl. x ∈ plane_of sctn} ∩ CX = {}"
assumes "guards ∩ (CX ∪ CP) = {}"
assumes "XS0 ⊆ CX × UNIV"
assumes "closed ivl"
assumes "CX ⊆ Csafe"
shows "do_intersection_spec UNIV guards ivl sctn XS0 (P, CX ∪ CP)"
using assms
apply (auto simp: do_intersection_spec_def)
subgoal
apply (rule flowsto_poincare_trans, assumption, assumption)
subgoal by simp
subgoal by auto
subgoal using assms(3) by auto
subgoal by (auto intro!: closed_levelset_within continuous_intros simp: plane_of_def)
subgoal premises prems for x d
proof -
have [intro, simp]: "closed {x ∈ ivl. x ∈ plane_of sctn} " "closed {x ∈ ivl. x ∙ normal sctn = pstn sctn}"
by (auto intro!: closed_levelset_within continuous_intros simp: plane_of_def assms)
from flowsto_poincare_mapsto_trans_flowsto[OF ‹flowsto _ _ _ _› ‹poincare_mapsto _ _ _ _ _› _ _ order_refl]
have ft: "flowsto XS0 {0<..} (X1 ∪ CX × UNIV ∪ CP × UNIV) (fst ` P × UNIV)"
by auto
then have ret: "returns_to {x ∈ ivl. x ∙ normal sctn - pstn sctn = 0} x"
apply (rule returns_to_flowstoI[OF _ _ _ _ _ _ order_refl])
using prems by (auto simp: plane_of_def)
have pm: "poincare_map {x ∈ ivl. x ∙ normal sctn = pstn sctn} x ∈ fst ` P"
apply (rule poincare_map_mem_flowstoI[OF ft])
using prems by (auto simp: plane_of_def)
from pm prems have "∀⇩F x in at (poincare_map {x ∈ ivl. x ∙ normal sctn = pstn sctn} x) within
plane_of sctn. x ∈ ivl"
by auto
from ret have "isCont (return_time {x ∈ ivl. x ∙ normal sctn - pstn sctn = 0}) x"
apply (rule return_time_isCont_outside)
using prems pm
by (auto simp: eventually_at_filter plane_of_def intro!: assms derivative_eq_intros)
then show "isCont (return_time {x ∈ ivl. x ∈ plane_of sctn}) x" by (simp add: plane_of_def)
qed
subgoal by simp
done
done
lemma do_intersection_coll_flowsto[le]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
assumes ft: "flowsto X0 {0..} (CX0 × UNIV) X"
assumes X_subset: "X ⊆ CX0 × UNIV"
assumes X0_subset: "X0 ⊆ CX0 × UNIV" and CX0_safe: "CX0 ⊆ Csafe"
assumes ci: "closed ivl"
assumes disj: "ivl ∩ plane_of sctn ∩ CX0 = {}" "sctns ∩ CX0 = {}"
shows "do_intersection_coll sctns ivl sctn (X::'n eucl1 set) ≤
SPEC (λ(P1, P2, CX, X0s).
∃A.
do_intersection_spec UNIV sctns ivl sctn A (P1, CX0 ∪ CX) ∧
do_intersection_spec UNIV sctns ivl sctn A (P2, CX0 ∪ CX) ∧
flowsto (X0 - A) {0..} (CX0 × UNIV) X0s ∧
A ⊆ X0 ∧
P1 ∩ X0s = {} ∧
P2 ∩ X0s = {})"
apply (rule do_intersection_coll)
apply (rule wd)
proof (clarsimp, goal_cases)
case (1 P1 P2 CX R)
from ft have "flowsto X0 {0..} (CX0 × UNIV) (X - R ∪ R)"
by (rule flowsto_subset) auto
from flowsto_union_DiffE[OF this]
obtain A where AB: "A ⊆ X0"
and A: "flowsto A {0..} (CX0 × UNIV) (X - R)"
and B: "flowsto (X0 - A) {0..} (CX0 × UNIV) (R)"
by auto
have di: "do_intersection_spec UNIV sctns ivl sctn A (P1, CX0 ∪ CX)"
apply (rule do_intersection_flowsto_trans_outside[OF A 1(1)])
subgoal using 1 by simp
subgoal using disj by auto
subgoal using 1 disj by (auto simp: do_intersection_spec_def)
subgoal using X0_subset AB by (auto simp: do_intersection_spec_def)
subgoal using ci by simp
subgoal using CX0_safe .
done
then have "P1 ⊆ (ivl ∩ plane_of sctn) × UNIV"
by (auto simp: do_intersection_spec_def)
then have disjoint: "P1 ∩ R = {}"
using ‹R ⊆ X› disj X_subset
apply (auto simp: subset_iff)
by (metis (no_types, lifting) Int_iff disjoint_iff_not_equal)
have di2: "do_intersection_spec UNIV sctns ivl sctn A (P2, CX0 ∪ CX)"
apply (rule do_intersection_flowsto_trans_outside[OF A 1(2)])
subgoal using 1 by simp
subgoal using disj by auto
subgoal using 1 disj by (auto simp: do_intersection_spec_def)
subgoal using X0_subset AB by (auto simp: do_intersection_spec_def)
subgoal using ci by simp
subgoal using CX0_safe .
done
then have "P2 ⊆ (ivl ∩ plane_of sctn) × UNIV"
by (auto simp: do_intersection_spec_def)
then have "P2 ∩ R = {}"
using ‹R ⊆ X› disj X_subset
apply (auto simp: subset_iff)
by (metis (no_types, lifting) Int_iff disjoint_iff_not_equal)
from AB this disjoint di di2 B show ?case
by (auto simp:)
qed
lemma op_enlarge_ivl_sctn[le, refine_vcg]:
"op_enlarge_ivl_sctn ivl sctn d ≤ SPEC (λivl'. ivl ⊆ ivl')"
unfolding op_enlarge_ivl_sctn_def
apply refine_vcg
unfolding plane_of_def
apply (safe intro!: eventually_in_planerectI)
apply (auto intro!: simp: eucl_le[where 'a='a] inner_sum_left inner_Basis if_distrib
algebra_simps cong: if_cong)
done
lemma resolve_ivlplanes[le]:
assumes wd[refine_vcg]: "wd TYPE('a::enum rvec)"
assumes
"∀x∈Xg. case x of (I, G) ⇒ flowsto (XSf G) {0..} (CXS × UNIV) G"
"(⋃x∈Xg. snd x) ⊆ (Csafe - (ivlplanes ∪ guards)) × UNIV"
"CXS × UNIV ⊆ (Csafe - (ivlplanes ∪ guards)) × UNIV"
"(⋃a∈Xg. XSf (snd a)) ⊆ (CXS::'a rvec set) × UNIV"
"(⋃x∈Xg. snd x) ⊆ CXS × UNIV"
"(⋃x∈Xg. fst x) ⊆ ivlplanes ∪ guards"
shows "resolve_ivlplanes guards ivlplanes Xg ≤ SPEC (λPS.
CXS ∩ (guards ∪ ivlplanes) = {} ∧
CXS ⊆ Csafe ∧
(∃R0 P0. (⋃x∈PS. P0 x) ∪ (⋃x∈PS. R0 x) = (⋃a∈Xg. XSf (snd a))∧
(∀x∈PS. case x of (X, P1, P2, R, ivl, sctn, CX) ⇒
ivl ∩ plane_of sctn ⊆ ivlplanes ∧ closed ivl ∧
P0 (X, P1, P2, R, ivl, sctn, CX) ∩ R0 (X, P1, P2, R, ivl, sctn, CX) = {} ∧
R0 (X, P1, P2, R, ivl, sctn, CX) ⊆ (CXS × UNIV) ∧
flowsto (R0 (X, P1, P2, R, ivl, sctn, CX)) {0..} (CXS × UNIV) R ∧
do_intersection_spec UNIV guards ivl sctn (P0 (X, P1, P2, R, ivl, sctn, CX)) (P1, CXS ∪ CX) ∧
do_intersection_spec UNIV guards ivl sctn (P0 (X, P1, P2, R, ivl, sctn, CX)) (P2, CXS ∪ CX))))"
using assms
unfolding resolve_ivlplanes_def
apply clarsimp_all
apply (refine_vcg FORWEAK_mono_rule[where I="λXgs PS.
(∃R0 P0.
snd ` Xgs ⊆ fst ` PS ∧ fst ` PS ⊆ snd ` Xg ∧
(∀(X, P1, P2, R, ivl, sctn, CX) ∈ PS.
P0 (X, P1, P2, R, ivl, sctn, CX) ∪ R0 (X, P1, P2, R, ivl, sctn, CX) = XSf X
∧ ivl ∩ plane_of sctn ⊆ ivlplanes ∧ closed ivl
∧ P0 (X, P1, P2, R, ivl, sctn, CX) ∩ R0 (X, P1, P2, R, ivl, sctn, CX) = {}
∧ R0 (X, P1, P2, R, ivl, sctn, CX) ⊆ (CXS × UNIV)
∧ flowsto (R0 (X, P1, P2, R, ivl, sctn, CX)) {0..} (CXS × UNIV) R
∧ do_intersection_spec UNIV guards ivl sctn (P0 (X, P1, P2, R, ivl, sctn, CX)) (P1, CXS ∪ CX)
∧ do_intersection_spec UNIV guards ivl sctn (P0 (X, P1, P2, R, ivl, sctn, CX)) (P2, CXS ∪ CX)))"],
clarsimp_all)
using [[goals_limit=1]]
subgoal by auto
subgoal by auto
subgoal for a b c
apply (frule bspec, assumption, clarsimp)
apply (rule do_intersection_coll_flowsto)
apply (rule wd)
apply assumption
apply force
apply force
apply blast
apply assumption
subgoal premises prems
proof -
have "(b ∩ plane_of c, a) ∈ Xg" using prems by simp
with ‹(⋃x∈Xg. fst x) ⊆ ivlplanes ∪ guards›
have "b ∩ plane_of c ⊆ ivlplanes ∪ guards"
by (force simp: subset_iff)
then show ?thesis
using ‹CXS × UNIV ⊆ (Csafe - (ivlplanes ∪ guards)) × UNIV›
by auto
qed
subgoal by (auto simp: subset_iff)
subgoal apply (refine_vcg, clarsimp_all) apply force
apply (intro exI conjI)defer defer defer apply assumption+
apply simp
apply force
apply force
apply force
done
done
subgoal by (auto simp: subset_iff) blast
subgoal for a b c d e f R0 P0
apply (frule bspec, assumption, clarsimp)
apply (rule do_intersection_coll_flowsto)
apply (rule wd)
apply assumption
subgoal
apply (rule order_trans[where y="(⋃x∈Xg. snd x)"])
by auto
subgoal
apply (rule order_trans) defer apply assumption
by auto
subgoal by blast
subgoal by simp
subgoal premises prems
proof -
have "(d ∩ plane_of e, c) ∈ Xg" using prems by simp
with ‹(⋃x∈Xg. fst x) ⊆ ivlplanes ∪ guards›
have "d ∩ plane_of e ⊆ ivlplanes ∪ guards"
by (force simp: subset_iff)
then show ?thesis
using ‹CXS × UNIV ⊆ (Csafe - (ivlplanes ∪ guards)) × UNIV›
by auto
qed
subgoal by (auto simp: subset_iff)
subgoal
apply (refine_vcg, clarsimp_all)
subgoal by (auto simp: subset_iff)
subgoal by auto
subgoal for x1 x1' x2 x3 A
apply (rule exI[where x="R0((c, x1, x1', x3, d, e, x2):=(XSf c - A))"])
apply (rule exI[where x="P0((c, x1, x1', x3, d, e, x2):=A)"])
apply clarsimp
apply (rule conjI)
subgoal by auto
apply (rule conjI)
subgoal premises prems
using prems
apply (auto simp: subset_iff)
by fastforce
apply clarsimp
subgoal
apply (drule bspec, assumption)
apply (drule bspec, assumption)
by force
done
done
done
subgoal by (auto simp: subset_iff)
subgoal by (auto simp: subset_iff)
subgoal for a R0 P0
apply (rule exI[where x=R0])
apply (rule exI[where x=P0])
apply (rule conjI)
subgoal premises prems
proof -
note prems
show ?thesis
using prems(9,8)
by fastforce
qed
by auto
done
lemma poincare_onto[le, refine_vcg]:
assumes wd[refine_vcg]: "wd TYPE('a::enum rvec)"
assumes [refine_vcg]: "⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤
SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) X)"
assumes CXS0: "CXS0 ∩ (guards ∪ ivlplanes) = {}"
shows "poincare_onto ro symstart trap guards ivlplanes (XS0::'a eucl1 set) CXS0 ≤
SPEC (λPS.
(∃R0 P0.
⋃(P0 ` PS ∪ R0 ` PS) = XS0 - trap × UNIV ∧
(∀(X, P1, P2, R, ivl, sctn, CX, CXS) ∈ PS.
ivl ∩ plane_of sctn ⊆ ivlplanes ∧ closed ivl
∧ XS0 ⊆ CXS × UNIV ∧ CXS0 ⊆ CXS ∧ CXS ∩ (guards ∪ ivlplanes) = {}
∧ P0 (X, P1, P2, R, ivl, sctn, CX, CXS) ∩ R0 (X, P1, P2, R, ivl, sctn, CX, CXS) = {}
∧ R0 (X, P1, P2, R, ivl, sctn, CX, CXS) ⊆ CXS × UNIV
∧ flowsto (R0 (X, P1, P2, R, ivl, sctn, CX, CXS)) {0..} (CXS × UNIV) R
∧ do_intersection_spec UNIV guards ivl sctn (P0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P1, CXS ∪ CX)
∧ do_intersection_spec UNIV guards ivl sctn (P0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P2, CXS ∪ CX))
))"
unfolding poincare_onto_def autoref_tag_defs
using [[goals_limit=1]]
apply (refine_vcg, clarsimp_all)
apply (refine_vcg resolve_ivlplanes[OF wd])
subgoal by force
apply clarsimp
subgoal for a b c d R0 P0
apply (rule exI[where x="λ(X, P1, P2, R, ivl, sctn, CX, CXS). R0 (X, P1, P2, R, ivl, sctn, CX)"])
apply (rule exI[where x="λ(X, P1, P2, R, ivl, sctn, CX, CXS). P0 (X, P1, P2, R, ivl, sctn, CX)"])
apply (rule conjI)
subgoal premises prems
using ‹(⋃x∈d. P0 x) ∪ (⋃x∈d. R0 x) = (⋃x∈b. c (snd x)) - trap × UNIV›
by auto
subgoal
apply clarsimp
apply (drule bspec, assumption)+
apply (rule conjI, force)
apply (rule conjI, force)
apply (rule conjI, force)
apply (rule conjI)
subgoal using CXS0 by auto
apply (rule conjI, force)
apply (rule conjI, force)
apply (rule conjI)
subgoal by (auto intro: flowsto_subset)
subgoal
apply clarsimp
apply (rule conjI)
subgoal
apply (rule do_intersection_spec_subset2, assumption)
subgoal by force
subgoal by (force simp: do_intersection_spec_def)
subgoal using CXS0 by (auto simp: do_intersection_spec_def)
subgoal using CXS0 by (auto simp: do_intersection_spec_def)
subgoal by auto
done
subgoal
apply (rule do_intersection_spec_subset2, assumption)
subgoal by force
subgoal by (force simp: do_intersection_spec_def)
subgoal using CXS0 by (auto simp: do_intersection_spec_def)
subgoal using CXS0 by (auto simp: do_intersection_spec_def)
subgoal by auto
done
done
done
done
done
lemma empty_remainders[le, refine_vcg]:
"empty_remainders PS ≤ SPEC (λb. b ⟶ (∀(X, P1, P2, R, ivl, sctn, CX) ∈ PS. R = {}))"
unfolding empty_remainders_def
by (refine_vcg FORWEAK_mono_rule[where I="λXs b. b ⟶ (∀(X, P1, P2, R, ivl, sctn, CX) ∈ Xs. R = {})"])
auto
lemma poincare_onto_empty[le, refine_vcg]:
assumes wd[refine_vcg]: "wd TYPE('a::enum rvec)"
assumes CXS0: "CXS0 ∩ (guards ∪ ivlplanes) = {}"
shows "poincare_onto_empty ro guards ivlplanes (XS0::'a eucl1 set) CXS0 ≤
SPEC (λ(PS).
(∃R0 P0.
⋃(P0 ` PS ∪ R0 ` PS) = XS0 ∧
(∀(X, P1, P2, R, ivl, sctn, CX, CXS) ∈ PS.
ivl ∩ plane_of sctn ⊆ ivlplanes ∧ closed ivl
∧ XS0 ⊆ CXS × UNIV ∧ CXS0 ⊆ CXS ∧ CXS ∩ (guards ∪ ivlplanes) = {}
∧ P0 (X, P1, P2, R, ivl, sctn, CX, CXS) ∩ R0 (X, P1, P2, R, ivl, sctn, CX, CXS) = {}
∧ R0 (X, P1, P2, R, ivl, sctn, CX, CXS) ⊆ CXS × UNIV
∧ flowsto (R0 (X, P1, P2, R, ivl, sctn, CX, CXS)) {0..} (CXS × UNIV) R
∧ do_intersection_spec UNIV guards ivl sctn (P0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P1, CXS ∪ CX)
∧ do_intersection_spec UNIV guards ivl sctn (P0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P2, CXS ∪ CX))
))"
using CXS0
unfolding poincare_onto_empty_def autoref_tag_defs
by (refine_vcg) (auto intro!: flowsto_self)
lemma do_intersection_spec_union2:
assumes "do_intersection_spec S osctns ivl csctns a (b, c)"
"do_intersection_spec S osctns ivl csctns f (b, c)"
shows "do_intersection_spec S osctns ivl csctns (a ∪ f) (b, c)"
using do_intersection_spec_union[OF assms]
by auto
lemma poincare_onto2[le, refine_vcg]:
assumes wd[refine_vcg]: "wd TYPE('a::enum rvec)"
assumes [refine_vcg]: "⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤
SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) X)"
notes [refine_vcg_def] = op_set_ndelete_spec
shows "poincare_onto2 ro symstart trap guards ivlplanes (XS0::'a eucl1 set) ≤
SPEC (λ(PS).
(∃P0. ⋃(P0 ` PS) = XS0 - trap × UNIV ∧
(∀(s, X, P1, P2, R, ivl, sctn, CX, CXS) ∈ PS.
XS0 ⊆ CXS × UNIV ∧
do_intersection_spec UNIV guards ivl sctn (P0 (s, X, P1, P2, R, ivl, sctn, CX, CXS)) (P1, CXS ∪ CX) ∧
do_intersection_spec UNIV guards ivl sctn (P0 (s, X, P1, P2, R, ivl, sctn, CX, CXS)) (P2, CXS ∪ CX))))"
unfolding poincare_onto2_def autoref_tag_defs
apply (refine_vcg, clarsimp_all)
subgoal for PS R0 P0
apply (rule FORWEAK_mono_rule_empty[where I="λPS1 PS2.
(∃X0.
⋃(R0 ` PS1) ⊆ ⋃(X0 ` PS2) ∧
(∀(X, P1, P2, R, ivl, sctn, CX, CXS) ∈ PS2.
XS0 ⊆ CXS × UNIV ∧
do_intersection_spec UNIV guards ivl sctn (X0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P1, CXS ∪ CX) ∧
do_intersection_spec UNIV guards ivl sctn (X0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P2, CXS ∪ CX)))"])
subgoal by refine_vcg
subgoal by auto
subgoal by auto
subgoal
apply clarsimp
subgoal for c
apply (rule exI[where x=c])
apply (rule conjI)
apply (rule order_trans) prefer 2 apply assumption
apply (rule UN_mono) apply assumption apply (rule order_refl) apply assumption
done
done
subgoal for σ
apply (clarsimp)
subgoal for X0
apply (rule exI[where x="λ(b, x). (if b then X0 x else P0 x) ∩ XS0 - trap × UNIV "])
apply (rule conjI)
subgoal premises prems
using ‹(⋃x∈PS. P0 x) ∪ (⋃x∈PS. R0 x) = XS0 - trap × UNIV›
‹(⋃x∈PS. R0 x) ⊆ (⋃x∈σ. X0 x)›
by auto
subgoal by (auto intro: do_intersection_spec_subset)
done
done
apply clarsimp
subgoal for a b b' c d e f g h i j
apply (cases "c = {}")
subgoal by (auto intro!: exI[where x="j"])
subgoal
using [[goals_limit=1]]
apply clarsimp
apply refine_vcg
subgoal premises prems for k l
proof -
note prems
then show ?thesis
apply -
apply (drule bspec, assumption)+
apply clarsimp
subgoal premises prems
using ‹g ∩ (guards ∪ ⋃k) = {}› ‹l = k - {d ∩ plane_of e} ∨ l = k› ‹d ∩ plane_of e ⊆ ⋃k›
by auto
done
qed
apply simp
apply (drule bspec, assumption)
apply simp
apply (erule exE conjE)+
subgoal for k l m n p q
apply (subgoal_tac "⋀x. x ∈ m ⟹ p x = {}")
defer
subgoal for x
proof goal_cases
case 1
from 1(10,15,24)
show ?case
by (auto dest!: bspec[where x=x])
qed
apply simp
subgoal premises prems
proof -
note prems
from prems have "finite (q ` m)" "flowsto (R0 (a, b, b', c, d, e, f, g)) {0..} (g × UNIV) (⋃(q ` m))"
by auto
from flowsto_Union_funE[OF this]
obtain XGs where
XGs: "⋀G. G ∈ q ` m ⟹ flowsto (XGs G) {0..} (g × UNIV) G"
"R0 (a, b, b', c, d, e, f, g) = ⋃(XGs ` (q ` m))"
by metis
define q0 where "q0 = XGs o q"
have "case x of (X, P1, P2, R, ivl, sctn, CX, CXS) ⇒
do_intersection_spec UNIV guards ivl sctn (q0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P1, CXS ∪ CX) ∧
do_intersection_spec UNIV guards ivl sctn (q0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P2, CXS ∪ CX)"
if "x ∈ m"
for x
proof (clarsimp, goal_cases)
case (1 X P1 P2 R ivl sctn CX CXS)
with prems(10)[rule_format, OF ‹x ∈ m›] prems(15)[rule_format, OF ‹x ∈ m›] ‹_ = c›
have *: "R = {}"
"x = (X, P1, P2, {}, ivl, sctn, CX, CXS)"
"ivl ∩ plane_of sctn ⊆ ⋃l"
"closed ivl"
"c ⊆ CXS × UNIV"
"g ⊆ CXS"
"⋃(q ` m) ⊆ CXS × UNIV"
"CXS ∩ (guards ∪ ⋃l) = {}"
"p (X, P1, P2, {}, ivl, sctn, CX, CXS) = {}"
"p (X, P1, P2, R, ivl, sctn, CX, CXS) ⊆ CXS × UNIV"
"do_intersection_spec UNIV guards ivl sctn (q (X, P1, P2, {}, ivl, sctn, CX, CXS)) (P1, CXS ∪ CX)"
"do_intersection_spec UNIV guards ivl sctn (q (X, P1, P2, {}, ivl, sctn, CX, CXS)) (P2, CXS ∪ CX)"
by auto
have "do_intersection_spec UNIV guards ivl sctn (q0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P1, (CXS ∪ CX) ∪ (CXS ∪ CX))"
apply (rule do_intersection_flowsto_trans_outside)
apply (simp add: q0_def)
apply (rule flowsto_subset)
apply (rule XGs)
using ‹x ∈ m› apply (rule imageI)
using 1 apply force
apply force
using * apply force
apply (rule order_refl)
using * apply (auto intro!: *)[]
subgoal
using * ‹x ∈ m›
by (auto simp add: )
subgoal using * by (auto simp: do_intersection_spec_def)
subgoal using * by (auto simp: do_intersection_spec_def)
subgoal
proof -
have "q0 (X, P1, P2, R, ivl, sctn, CX, CXS) ⊆ XGs (q x)"
by (auto simp: q0_def 1)
also have "… ⊆ R0 (a, b, b', c, d, e, f, g)" using ‹x ∈m› XGs by auto
also have "… ⊆ (CXS ∪ CX) × UNIV"
using prems(20) ‹g ⊆ CXS› by auto
finally show ?thesis by simp
qed
subgoal by fact
subgoal using * by (auto simp: do_intersection_spec_def)
done
moreover have "do_intersection_spec UNIV guards ivl sctn (q0 (X, P1, P2, R, ivl, sctn, CX, CXS)) (P2, (CXS ∪ CX) ∪ (CXS ∪ CX))"
apply (rule do_intersection_flowsto_trans_outside)
apply (simp add: q0_def)
apply (rule flowsto_subset)
apply (rule XGs)
using ‹x ∈ m› apply (rule imageI)
using 1 apply force
apply force
using * apply force
apply (rule order_refl)
using * apply (auto intro!: *)[]
subgoal
using * ‹x ∈ m›
by (auto simp add: )
subgoal using * by (auto simp: do_intersection_spec_def)
subgoal using * by (auto simp: do_intersection_spec_def)
subgoal
proof -
have "q0 (X, P1, P2, R, ivl, sctn, CX, CXS) ⊆ XGs (q x)"
by (auto simp: q0_def 1)
also have "… ⊆ R0 (a, b, b', c, d, e, f, g)" using ‹x ∈m› XGs by auto
also have "… ⊆ (CXS ∪ CX) × UNIV"
using prems(20) ‹g ⊆ CXS› by auto
finally show ?thesis by simp
qed
subgoal by fact
subgoal using * by (auto simp: do_intersection_spec_def)
done
ultimately show ?case
by simp
qed note q0 = this
have q0': "(a, aa, aa', ab, ac, ad, ae, b) ∈ m ⟹ XS0 ⊆ b × UNIV" for a aa aa' ab ac ad ae b
apply (drule prems(15)[rule_format])
using ‹XS0 ⊆ g × UNIV›
by auto
from prems
show ?thesis
apply (intro exI[where x="λx. if x ∈ i ∩ m then j x ∪ q0 x else if x ∈ i then j x else q0 x"] conjI)
subgoal 1 premises prems
unfolding XGs
apply simp
by (auto simp: q0_def)
subgoal premises _
by (rule order_trans[OF ‹(⋃x∈h. R0 x) ⊆ (⋃x∈i. j x)›]) auto
subgoal premises _ using prems(6)[rule_format] q0
apply auto
subgoal by (auto dest!: prems(6)[rule_format] q0 intro!: do_intersection_spec_union2)
subgoal by (auto dest!: prems(6)[rule_format] q0 intro!: do_intersection_spec_union2)
subgoal by (auto intro!: do_intersection_spec_union2)
subgoal by (auto dest!: prems(6)[rule_format] q0' intro!: do_intersection_spec_union2)
subgoal by (auto dest!: prems(6)[rule_format] q0 intro!: do_intersection_spec_union2)
subgoal by (auto dest!: prems(6)[rule_format] q0 intro!: do_intersection_spec_union2)
subgoal by (auto dest!: prems(6)[rule_format] q0 intro!: do_intersection_spec_union2)
subgoal by (auto dest!: prems(6)[rule_format] q0 intro!: do_intersection_spec_union2)
done
done
qed
done
done
done
done
done
lemma width_spec_ivl[THEN order_trans, refine_vcg]: "width_spec_ivl M X ≤ SPEC (λx. True)"
unfolding width_spec_ivl_def
by (refine_vcg)
lemma partition_ivl_spec[le, refine_vcg]:
shows "partition_ivl cg XS ≤ SPEC (λYS. XS ⊆ YS)"
using [[simproc del: defined_all]]
unfolding partition_ivl_def autoref_tag_defs
apply (refine_vcg, clarsimp_all)
subgoal by fastforce
subgoal by fastforce
subgoal by fastforce
subgoal by fastforce
subgoal premises prems for a b c d e f ws g h i j k l m n
proof -
note prems
have disj: "⋀A Aa. n ∉ A ∨ ¬ XS ∩ A ⊆ Aa ∨ n ∈ Aa"
using prems by blast
then have "n ∈ g"
using prems by (metis (no_types) Un_iff atLeastAtMost_iff subset_iff)
then show ?thesis
using disj prems by (meson atLeastAtMost_iff)
qed
done
lemma op_inter_fst_ivl_scaleR2[le,refine_vcg]:
"op_inter_fst_ivl_scaleR2 X Y ≤ SPEC (λR. X ∩ (Y × UNIV) = R)"
unfolding op_inter_fst_ivl_scaleR2_def
apply refine_vcg
apply (auto simp: scaleR2_def)
subgoal for a b c d e f g h i j k
by (rule image_eqI[where x="(i, (j, k))"]; fastforce)
subgoal for a b c d e f g h i j k
by (rule image_eqI[where x="(i, (j, k))"]; fastforce)
done
lemma op_inter_fst_ivl_coll_scaleR2[le,refine_vcg]:
"op_inter_fst_ivl_coll_scaleR2 X Y ≤ SPEC (λR. X ∩ (Y × UNIV) = R)"
unfolding op_inter_fst_ivl_coll_scaleR2_def
by (refine_vcg FORWEAK_mono_rule[where I="λXs R. (⋃Xs) ∩ (Y × UNIV) ⊆ R ∧ R ⊆ X ∩ (Y × UNIV)"])
auto
lemma op_inter_ivl_co[le, refine_vcg]: "op_ivl_of_ivl_coll X ≤ SPEC (λR. X ⊆ R)"
unfolding op_ivl_of_ivl_coll_def
apply (refine_vcg FORWEAK_mono_rule[where I="λR (l, u). ⋃R ⊆ {l .. u}"])
apply auto
apply (metis Set.basic_monos(7) Sup_le_iff atLeastAtMost_iff inf.coboundedI2 inf_sup_aci(1))
by (meson Set.basic_monos(7) UnionI atLeastAtMost_iff le_supI1)
lemma op_inter_ivl_coll_scaleR2[le,refine_vcg]:
"op_inter_ivl_coll_scaleR2 X Y ≤ SPEC (λR. X ∩ (Y × UNIV) ⊆ R)"
unfolding op_inter_ivl_coll_scaleR2_def
apply refine_vcg
subgoal for _ _ _ A l u
by (auto, rule scaleR2_subset[where i'=l and j'=u and k'=A], auto)
done
lemma [le, refine_vcg]: "op_image_fst_ivl_coll X ≤ SPEC (λR. R = fst ` X)"
unfolding op_image_fst_ivl_coll_def
apply (refine_vcg FORWEAK_mono_rule[where I="λXs R. fst ` (⋃Xs) ⊆ R ∧ R ⊆ fst ` X"])
apply auto
apply force+
done
lemma op_single_inter_ivl[le, refine_vcg]: "op_single_inter_ivl a fxs ≤ SPEC (λR. a ∩ fxs ⊆ R)"
unfolding op_single_inter_ivl_def
by refine_vcg auto
lemma partition_ivle_spec[le, refine_vcg]:
shows "partition_ivle cg XS ≤ SPEC (λYS. XS ⊆ YS)"
unfolding partition_ivle_def autoref_tag_defs
supply [refine_vcg del] = scaleR2_rep_of_coll2
and [refine_vcg] = scaleR2_rep_of_coll
apply (refine_vcg)
subgoal by (fastforce simp: scaleR2_def)
subgoal by auto
apply clarsimp
subgoal by (fastforce simp: scaleR2_def)
done
lemma vec1repse[THEN order_trans, refine_vcg]:
"vec1repse CX ≤ SPEC (λR. case R of None ⇒ True | Some X ⇒ X = vec1_of_flow1 ` CX)"
unfolding vec1repse_def
apply (refine_vcg FORWEAK_mono_rule[where
I="λXS R. case R of None ⇒ True | Some R ⇒ vec1_of_flow1 ` (⋃XS) ⊆ R ∧ R ⊆ vec1_of_flow1 ` CX"])
apply (auto simp: scaleR2_def split: option.splits)
subgoal for a b c d e f g h i j
apply (auto simp: vimage_def image_def)
apply (rule exI[where x="h"])
apply auto
apply (rule exI[where x=f])
apply (rule exI[where x="matrix j"])
apply auto
apply (rule bexI)
by (auto simp: vec1_of_flow1_def matrix_scaleR)
subgoal for a b c d e f g h i j
apply (rule bexI)
defer apply assumption
apply (rule image_eqI[where x="(f, g, j)"])
by (auto simp: flow1_of_vec1_def vec1_of_flow1_def matrix_scaleR[symmetric])
subgoal by fastforce
subgoal for a b c d e f g h i j k l
apply (auto simp: vimage_def image_def)
apply (rule exI[where x="j"])
apply auto
apply (rule exI[where x=h])
apply (rule exI[where x="matrix l"])
apply auto
apply (rule bexI)
by (auto simp: vec1_of_flow1_def matrix_scaleR)
subgoal by fastforce
subgoal for a b c d e f g h i j k l
apply (rule bexI)
defer apply assumption
apply (rule image_eqI[where x="(h, i, l)"])
by (auto simp: flow1_of_vec1_def vec1_of_flow1_def matrix_scaleR[symmetric])
done
lemma scaleR2_rep1[le, refine_vcg]: "scaleR2_rep1 Y ≤ SPEC (λR. Y ⊆ R)"
unfolding scaleR2_rep1_def
apply refine_vcg
subgoal by (auto simp: norm2_slp_def)
subgoal for a b c d e y z f g h i j prec k l m n p q r s
apply (auto simp: scaleR2_def image_def vimage_def)
subgoal premises prems for B C D E
proof -
define ij where "ij = (i + j) / 2"
from prems
have "ij > 0"
by (auto simp: ij_def)
show ?thesis
unfolding ij_def[symmetric]
apply (rule exI[where x="1 / ij * B"])
apply (intro conjI) prefer 3
apply (rule bexI[where x="(D, ij *⇩R E)"])
subgoal using ‹ij > 0› by auto
subgoal
using prems
using ‹(D, E) ∈ c› ‹c ⊆ {(n, p)..(q, r)}› ‹ij > 0›
by (auto simp: ij_def[symmetric] intro!: scaleR_left_mono)
subgoal
using ‹d ≤ ereal B› ‹0 < ij› ‹0 < d›
apply (cases d)
apply (simp only: times_ereal.simps ereal_less_eq)
apply (rule mult_mono)
apply (rule real_divl)
by auto
subgoal
using ‹0 < d› ‹d ≤ ereal B› ‹ereal B ≤ e› ‹0 < ij› ‹0 < e›
‹0 < real_divr prec 1 ((i + j) / 2)›
unfolding ij_def[symmetric]
apply (cases e; cases d)
apply (simp only: times_ereal.simps ereal_less_eq)
apply (rule mult_mono)
apply (rule real_divr)
by auto
done
qed
done
done
lemma reduce_ivl[le, refine_vcg]: "reduce_ivl Y b ≤ SPEC (λR. Y ⊆ R)"
unfolding reduce_ivl_def
apply refine_vcg
apply (auto simp add: scaleR2_def image_def vimage_def plane_of_def )
proof goal_cases
case (1 i0 i1 s0 s1 y0 y1)
from 1 have le: "1 ≤ (y1 ∙ b) / (i1 ∙ b)"
by (auto simp: min_def dest!: inner_Basis_mono[OF _ ‹b ∈ Basis›])
show ?case
apply (rule exI[where x="(y1 ∙ b) / (i1 ∙ b)"])
apply (rule conjI) apply fact
apply (rule bexI[where x="(y0, ((i1 ∙ b) / (y1 ∙ b)) *⇩R y1)"])
subgoal using 1 le by simp
subgoal using 1 le apply simp
apply (rule conjI)
subgoal
apply (auto simp: eucl_le[where 'a="'c"])
apply (auto simp: divide_simps)
apply (subst mult.commute)
subgoal for i
apply (cases " y1 ∙ b ≤ i1 ∙ b")
apply (rule order_trans)
apply (rule mult_left_mono[where b="y1 ∙ i"])
apply (auto simp: mult_le_cancel_right)
apply (cases "i1 ∙ i ≤ 0")
apply (rule order_trans)
apply (rule mult_right_mono_neg[where b="i1 ∙ b"])
apply auto
by (auto simp: not_le inner_Basis split: if_splits dest!: bspec[where x=i])
done
subgoal
apply (auto simp: eucl_le[where 'a="'c"])
subgoal for i
apply (cases "i = b")
apply (auto simp: divide_simps)
subgoal by (auto simp: divide_simps algebra_simps)
subgoal apply (auto simp: divide_simps algebra_simps inner_Basis)
apply (subst mult.commute)
apply (rule order_trans)
apply (rule mult_right_mono[where b="s1 ∙ i"]) apply simp
apply simp
apply (rule mult_left_mono)
by auto
done
done
done
done
next
case (2 i0 i1 s0 s1 y0 y1)
from 2 have le: "1 ≤ (y1 ∙ b) / (s1 ∙ b)"
by (auto simp: min_def abs_real_def divide_simps dest!: inner_Basis_mono[OF _ ‹b ∈ Basis›])
show ?case
apply (rule exI[where x="(y1 ∙ b) / (s1 ∙ b)"])
apply (rule conjI) apply fact
apply (rule bexI[where x="(y0, ((s1 ∙ b) / (y1 ∙ b)) *⇩R y1)"])
subgoal using 2 le by simp
subgoal using 2 le apply simp
apply (rule conjI)
subgoal
apply (auto simp: eucl_le[where 'a="'c"])
subgoal for i
apply (cases "i = b")
apply (auto simp: divide_simps)
subgoal by (auto simp: divide_simps algebra_simps)
subgoal apply (auto simp: divide_simps algebra_simps inner_Basis)
apply (subst mult.commute)
apply (cases "y1 ∙ i ≤ 0")
apply (rule order_trans)
apply (rule mult_left_mono_neg[where b="y1 ∙ b"])
apply (auto simp: mult_le_cancel_right not_le)
apply (rule order_trans)
apply (rule mult_right_mono_neg[where b="i1 ∙ i"])
apply (auto intro!: mult_left_mono_neg)
done
done
done
subgoal
apply (auto simp: eucl_le[where 'a="'c"])
subgoal for i
apply (cases "i = b")
subgoal by (auto simp: divide_simps algebra_simps)
subgoal apply (auto simp: divide_simps algebra_simps inner_Basis)
apply (subst mult.commute)
apply (cases "y1 ∙ i ≥ 0")
apply (rule order_trans)
apply (rule mult_left_mono_neg[where b="y1 ∙ i"]) apply simp
apply simp
apply (rule mult_right_mono) apply force
apply force
proof -
assume a1: "∀i∈Basis. s1 ∙ b * (if b = i then 1 else 0) ≤ s1 ∙ i"
assume a2: "i ∈ Basis"
assume a3: "i ≠ b"
assume a4: "y1 ∙ b < 0"
assume a5: "s1 ∙ b < 0"
assume a6: "¬ 0 ≤ y1 ∙ i"
have "s1 ∙ b * (if b = i then 1 else 0) ≤ s1 ∙ i"
using a2 a1 by metis
then have f7: "0 ≤ s1 ∙ i"
using a3 by (metis (full_types) mult_zero_right)
have f8: "y1 ∙ b ≤ 0"
using a4 by (metis eucl_less_le_not_le)
have "s1 ∙ b ≤ 0"
using a5 by (metis eucl_less_le_not_le)
then show "y1 ∙ b * (s1 ∙ i) ≤ s1 ∙ b * (y1 ∙ i)"
using f8 f7 a6 by (metis mult_right_mono_le mult_zero_left zero_le_mult_iff zero_le_square)
qed
done
done
done
done
qed
lemma reduce_ivle[le, refine_vcg]:
"reduce_ivle Y b ≤ SPEC (λR. Y ⊆ R)"
using [[simproc del: defined_all]]
unfolding reduce_ivle_def
apply refine_vcg
apply (auto simp: scaleR2_def image_def vimage_def)
subgoal for a b c d e f g h i j k
apply (drule subsetD, assumption)
apply auto
subgoal for l m
apply (rule exI[where x="l * g"])
apply (intro conjI)
subgoal
unfolding times_ereal.simps[symmetric]
apply (rule ereal_mult_mono)
subgoal by (cases e) auto
subgoal by (cases b) auto
subgoal by (cases b) auto
subgoal by (cases e) auto
done
subgoal
unfolding times_ereal.simps[symmetric]
apply (rule ereal_mult_mono)
subgoal by (cases b) auto
subgoal by (cases b) auto
subgoal by (cases b) auto
subgoal by (cases e) auto
done
subgoal by force
done
done
done
lemma reduces_ivle[le, refine_vcg]:
"reduces_ivle X ≤ SPEC (λR. X ⊆ R)"
unfolding reduces_ivle_def
by refine_vcg auto
lemma ivlse_of_setse[le, refine_vcg]: "ivlse_of_setse X ≤ SPEC (λR. X ⊆ R)"
unfolding ivlse_of_setse_def
by (refine_vcg FORWEAK_mono_rule[where I="λXs R. ⋃Xs ⊆ R"])
(auto simp: scaleR2_def image_def vimage_def)
lemma setse_of_ivlse[le, refine_vcg]:
"setse_of_ivlse X ≤ SPEC (λR. R = X)"
unfolding setse_of_ivlse_def
apply (refine_vcg FORWEAK_mono_rule[where I="λXs R. ⋃Xs ⊆ R ∧ R ⊆ X"])
apply clarsimp_all
subgoal by (rule bexI)
subgoal by auto
subgoal by auto
subgoal by auto
done
lemma partition_set_spec[le, refine_vcg]:
shows "partition_set ro XS ≤ SPEC (λYS. XS ⊆ YS)"
unfolding partition_set_def autoref_tag_defs
apply (refine_vcg)
subgoal by (fastforce simp: scaleR2_def vimage_def image_def)
subgoal by fastforce
done
lemma partition_sets_spec[le, refine_vcg]:
shows "partition_sets ro XS ≤ SPEC (λYS. (⋃(_, _, PS, _, _, _, _, _) ∈ XS. PS) ⊆ YS)"
unfolding partition_sets_def autoref_tag_defs
by (refine_vcg FORWEAK_mono_rule[where I="λX Y. (⋃(_, _, PS, _, _, _, _, _) ∈ X. PS) ⊆ Y"]) auto
lemma
do_intersection_poincare_mapstos_trans:
assumes pm: "⋀i. i ∈ I ⟹ poincare_mapsto (p i) (X0 i) UNIV (CX i) (X1 i)"
assumes di: "do_intersection_spec UNIV guards ivl sctn (⋃i∈I. X1 i) (P, CP)"
assumes "⋀i. i ∈ I ⟹ fst ` (X1 i) ⊆ CP"
assumes "⋀i. i ∈ I ⟹ {x ∈ ivl. x ∈ plane_of sctn} ∩ CX i = {}"
assumes "⋀i. i ∈ I ⟹ guards ∩ (CX i ∪ CP) = {}"
assumes "⋀i. i ∈ I ⟹ X0 i ⊆ CX i × UNIV"
assumes "⋀i. i ∈ I ⟹ closed (p i)"
assumes "closed ivl"
assumes "⋀i. i ∈ I ⟹ CX i ⊆ Csafe"
shows "do_intersection_spec UNIV guards ivl sctn (⋃i∈I. X0 i) (P, (⋃i∈I. CX i) ∪ CP)"
apply (auto simp: do_intersection_spec_def)
subgoal
apply (simp del: UN_simps add: UN_extend_simps)
apply (rule impI)
apply (thin_tac "I ≠ {}")
subgoal
proof -
from di have pmi: "poincare_mapsto {x ∈ ivl. x ∈ plane_of sctn} (X1 i) UNIV CP P" if "i ∈ I" for i
by (auto simp: do_intersection_spec_def intro: poincare_mapsto_subset that)
show ?thesis
apply (rule poincare_mapsto_UnionI)
apply (rule poincare_mapsto_trans[OF pm pmi])
apply clarsimp_all
subgoal s1 using assms by (auto simp: do_intersection_spec_def)
subgoal using assms apply (auto simp: do_intersection_spec_def)
apply blast
by (metis (mono_tags, lifting) s1 mem_Collect_eq mem_simps(2) mem_simps(4))
subgoal using assms by auto
subgoal using assms by auto
subgoal premises prems for i x d
proof -
note prems
have [intro, simp]: "closed {x ∈ ivl. x ∈ plane_of sctn} " "closed {x ∈ ivl. x ∙ normal sctn = pstn sctn}"
by (auto intro!: closed_levelset_within continuous_intros simp: plane_of_def assms)
have set_eq: "(CX i ∪ CP) × UNIV = (fst ` X1 i × UNIV ∪ CX i × UNIV ∪ CP × UNIV)"
using assms prems
by auto
have empty_inter: "{x ∈ ivl. x ∙ normal sctn - pstn sctn = 0} × UNIV ∩ (CX i ∪ CP) × UNIV = {}"
apply safe
subgoal
using assms(4)[of i] ‹i ∈ I›
by (auto simp: plane_of_def )
subgoal
using assms(4)[of i]
using prems assms by (auto simp: plane_of_def do_intersection_spec_def)
done
have ft: "flowsto (X0 i) {0<..} ((CX i ∪ CP) × UNIV) (fst ` P × UNIV)"
unfolding set_eq
apply (rule flowsto_poincare_mapsto_trans_flowsto[OF poincare_mapsto_imp_flowsto[OF pm[OF ‹i ∈ I›]]
pmi[OF ‹i ∈ I›] _ _ order_refl])
using assms prems by (auto)
then have ret: "returns_to {x ∈ ivl. x ∙ normal sctn - pstn sctn = 0} x"
apply (rule returns_to_flowstoI[OF _ _ _ _ _ _ order_refl])
subgoal using prems assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal by (rule empty_inter)
subgoal using prems assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using prems assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using prems assms by (auto simp: plane_of_def do_intersection_spec_def)
done
have pm: "poincare_map {x ∈ ivl. x ∙ normal sctn = pstn sctn} x ∈ fst ` P"
apply (rule poincare_map_mem_flowstoI[OF ft])
subgoal using prems assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using empty_inter by simp
subgoal by auto
subgoal by auto
subgoal using prems assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal by auto
done
from ret have "isCont (return_time {x ∈ ivl. x ∙ normal sctn - pstn sctn = 0}) x"
apply (rule return_time_isCont_outside)
subgoal by fact
apply (force intro!: derivative_eq_intros)
subgoal by (auto intro!: continuous_intros)
subgoal using prems pm assms by (auto simp: do_intersection_spec_def)
subgoal using prems pm assms
by (auto simp: eventually_at_filter plane_of_def do_intersection_spec_def)
subgoal
proof -
have "x ∈ CX i" using ‹_ ∈ I ⟹ X0 _ ⊆ CX _ × UNIV›[OF ‹i ∈ I›] ‹(x, _) ∈ _›
by auto
with assms(4)[OF ‹i ∈ I›] show ?thesis
by (auto simp: plane_of_def)
qed
done
then show "isCont (return_time {x ∈ ivl. x ∈ plane_of sctn}) x" by (simp add: plane_of_def)
qed
done
qed
done
subgoal using assms by (fastforce simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (fastforce simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using assms(9) by (fastforce simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
subgoal using assms by (auto simp: plane_of_def do_intersection_spec_def)
done
lemma flow_in_stable_setD:
"flow0 x0 t ∈ stable_set trap ⟹ t ∈ existence_ivl0 x0 ⟹ x0 ∈ stable_set trap"
apply (auto simp: stable_set_def)
proof goal_cases
case (1 s)
then show ?case
apply (cases "s ≤ t")
apply (meson atLeastAtMost_iff contra_subsetD local.ivl_subset_existence_ivl)
using contra_subsetD local.existence_ivl_reverse local.existence_ivl_trans' local.flows_reverse by fastforce
next
case (2)
have "((λs. flow0 x0 (t + s)) ⤏ trap) (at_top)"
proof (rule Lim_transform_eventually)
have "∀⇩F x in at_top. x > max t 0"
by (simp add: max_def)
then show "∀⇩F x in at_top. flow0 (flow0 x0 t) x = flow0 x0 (t + x)"
apply eventually_elim
apply (subst flow_trans)
using 2
by auto
qed (use 2 in auto)
then show ?case by (simp add: tendsto_at_top_translate_iff ac_simps)
qed
lemma
poincare_mapsto_avoid_trap:
assumes "poincare_mapsto p (X0 - trap × UNIV) S CX P"
assumes "closed p"
assumes trapprop[THEN stable_onD]: "stable_on (CX ∪ fst ` P) trap"
shows "poincare_mapsto p (X0 - trap × UNIV) S CX (P - trap × UNIV)"
using assms(1,2)
apply (auto simp: poincare_mapsto_def)
apply (drule bspec, force)
apply auto
subgoal for x0 d0 D
apply (rule exI[where x=D])
apply (auto dest!: trapprop simp: poincare_map_def intro!: return_time_exivl assms(1,2) return_time_pos)
subgoal for s
by (cases "s = return_time p x0") auto
done
done
lemma poincare_onto_series[le, refine_vcg]:
assumes wd[refine_vcg]: "wd TYPE('a::enum rvec)"
assumes [refine_vcg]: "⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤ SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
assumes trapprop: "stable_on (Csafe - (ivl ∩ plane_of sctn)) trap"
shows "poincare_onto_series symstart trap guards (X0::'a eucl1 set) ivl sctn ro ≤
SPEC (λXS. do_intersection_spec UNIV {} ivl sctn (X0 - trap × UNIV)
(XS, Csafe - (ivl ∩ plane_of sctn)) ∧
fst ` X0 - trap ⊆ Csafe - (ivl ∩ plane_of sctn))"
proof (induction guards arbitrary: X0)
case Nil
then show ?case
apply (simp add:)
apply refine_vcg
apply (clarsimp simp add: ivlsctn_to_set_def)
apply (rule do_intersection_spec_subset2, assumption)
subgoal by (auto simp: do_intersection_spec_def)
subgoal by (auto simp: do_intersection_spec_def)
subgoal by (auto simp: do_intersection_spec_def)
subgoal by (auto simp: do_intersection_spec_def)
subgoal by (auto simp: do_intersection_spec_def)
subgoal by (auto simp: do_intersection_spec_def)
done
next
case (Cons a guards)
note Cons.IH[simplified, le, refine_vcg]
show ?case
supply [[simproc del: defined_all]]
apply auto
apply refine_vcg
apply clarsimp_all
defer
subgoal premises prems for b c d e f g h
proof -
from prems have "(f, g) ∈ (⋃x∈c. h x)"
by auto
then obtain x where "x ∈ c" "(f, g) ∈ (h x)"
by auto
then show ?thesis
using prems(14)[rule_format, OF ‹x ∈ c›] prems(5-7)
by (cases x) (auto simp: do_intersection_spec_def)
qed
subgoal premises prems for c ro d e f
proof -
let ?s = "trap × UNIV"
note prems
from ‹do_intersection_spec _ _ _ _ _ _ ›
have disro: "do_intersection_spec UNIV {} ivl sctn ((⋃i∈ro. case i of (_, _, PS, _, _, _, _, _, _) ⇒ PS - ?s))
(e, Csafe - ivl ∩ plane_of sctn)"
apply (rule do_intersection_spec_subset)
using prems by auto
have subset: "(Csafe - ivl ∩ plane (normal sctn) (pstn sctn)) ⊇
(snd (snd (snd (snd (snd (snd (snd (snd i))))))) ∪
fst (snd (snd (snd (snd (snd (snd (snd i))))))) ∪ fst ` fst (snd (snd i)))" if "i ∈ ro" for i
using prems(12)[rule_format, unfolded do_intersection_spec_def, OF that]
apply (clarsimp )
subgoal for s X P1 P2 R ivla sctna CX CXS
apply (rule conjI)
subgoal by (auto simp: plane_of_def)
subgoal by (auto simp: plane_of_def)
done
done
have pmro: "poincare_mapsto
(case i of (s, X, P1, P2, R, ivla, sctna, CX, CXS) ⇒ {x ∈ ivla. x ∈ plane_of sctna})
(f i - ?s) UNIV
(case i of (s, X, P1, P2, R, ivla, sctna, CX, CXS) ⇒ CXS ∪ CX)
(case i of (s, X, P1, P2, R, ivla, sctna, CX, CXS) ⇒ P1)"
if "i ∈ ro"
for i
using prems(12)[rule_format, unfolded do_intersection_spec_def, OF that]
by (auto intro: poincare_mapsto_subset)
then have pmro: "poincare_mapsto
(case i of (s, X, P1, P2, R, ivla, sctna, CX, CXS) ⇒ {x ∈ ivla. x ∈ plane_of sctna})
(f i - ?s) UNIV
(case i of (s, X, P1, P2, R, ivla, sctna, CX, CXS) ⇒ CXS ∪ CX)
(case i of (s, X, P1, P2, R, ivla, sctna, CX, CXS) ⇒ P1 - ?s)"
if "i ∈ ro"
for i
unfolding split_beta'
apply (rule poincare_mapsto_avoid_trap)
using that prems assms
by (auto intro!: closed_levelset_within continuous_intros
stable_on_mono[OF _ subset]
simp: plane_of_def)
have "do_intersection_spec UNIV {} ivl sctn (⋃i∈ro. f i - ?s)
(e, (⋃i∈ro. case i of (s, X, P1, P2, R, ivla, sctna, CX, CXS) ⇒ CXS ∪ CX) ∪
(Csafe - ivl ∩ plane_of sctn))"
apply (rule do_intersection_poincare_mapstos_trans[OF pmro disro])
subgoal by auto
subgoal premises that for i
using prems(12)[rule_format, unfolded do_intersection_spec_def, OF that] using [[simproc del: defined_all]]
by (auto simp: do_intersection_spec_def)
subgoal using assms(1,2) prems by (auto simp: do_intersection_spec_def)
subgoal by auto
subgoal premises that for i
using prems(12)[rule_format, unfolded do_intersection_spec_def, OF that]
prems(11) that
by (auto simp: do_intersection_spec_def)
subgoal using assms(1,2) prems by (auto simp: do_intersection_spec_def)
subgoal using assms(1,2) prems by (auto simp: do_intersection_spec_def)
subgoal using assms(1,2) prems by (auto simp: do_intersection_spec_def)
done
then show ?thesis
unfolding ‹(⋃x∈ro. f x) = X0 - trap × UNIV›
apply (rule do_intersection_spec_subset2)
subgoal using assms(1,2) prems by (auto simp: do_intersection_spec_def)
using prems
by (auto simp: do_intersection_spec_def intro: poincare_mapsto_subset)
qed
done
qed
lemma
do_intersection_flowsto_trans_return:
assumes "flowsto XS0 {0<..} (CX × UNIV) X1"
assumes "do_intersection_spec UNIV guards ivl sctn X1 (P, CP)"
assumes "fst ` X1 ⊆ CP"
assumes "{x ∈ ivl. x ∈ plane_of sctn} ∩ CX = {}"
assumes "guards ∩ (CX ∪ CP) = {}"
assumes "closed ivl"
assumes "CX ⊆ sbelow_halfspace sctn ∩ Csafe"
assumes subset_plane: "fst ` XS0 ⊆ plane_of sctn ∩ ivl"
assumes down: "⋀x d. (x, d) ∈ XS0 ⟹ ode x ∙ normal sctn < 0" "⋀x. x ∈ CX ⟹ ode x ∙ normal sctn < 0"
shows "do_intersection_spec (below_halfspace sctn) guards ivl sctn XS0 (P, CX ∪ CP)"
using assms
apply (auto simp: do_intersection_spec_def)
subgoal
apply (rule flowsto_poincare_trans, assumption, assumption)
subgoal by simp
subgoal by auto
subgoal using assms(3) by auto
subgoal by (auto intro!: closed_levelset_within continuous_intros simp: plane_of_def)
prefer 2
subgoal by (auto simp add: plane_of_def halfspace_simps)
subgoal premises prems for x d
proof -
have [intro, simp]: "closed {x ∈ ivl. x ∈ plane_of sctn} " "closed {x ∈ ivl. x ∙ normal sctn = pstn sctn}"
by (auto intro!: closed_levelset_within continuous_intros simp: plane_of_def assms)
from subset_plane have "fst ` XS0 ⊆ below_halfspace sctn" by auto
from flowsto_stays_sbelow[OF ‹flowsto _ _ _ _› this down(2)]
have ft_below: "flowsto XS0 pos_reals (CX × UNIV ∩ sbelow_halfspace sctn × UNIV) X1"
by auto
from flowsto_poincare_mapsto_trans_flowsto[OF ft_below ‹poincare_mapsto _ _ _ _ _› _ _ order_refl]
have ft: "flowsto XS0 {0<..} (X1 ∪ CX × UNIV ∩ sbelow_halfspace sctn × UNIV ∪ CP × UNIV) (fst ` P × UNIV)"
by auto
have ret: "returns_to {x ∈ ivl. x ∙ normal sctn - pstn sctn = 0} x"
apply (rule returns_to_flowstoI[OF ft])
using prems by (auto simp: plane_of_def halfspace_simps)
have pm: "poincare_map {x ∈ ivl. x ∙ normal sctn = pstn sctn} x ∈ fst ` P"
apply (rule poincare_map_mem_flowstoI[OF ft])
using prems by (auto simp: plane_of_def halfspace_simps)
from pm prems have evmem: "∀⇩F x in at (poincare_map {x ∈ ivl. x ∙ normal sctn = pstn sctn} x) within
plane_of sctn. x ∈ ivl"
by auto
from ret have "continuous (at x within {x. x ∙ normal sctn - pstn sctn ≤ 0})
(return_time {x ∈ ivl. x ∙ normal sctn - pstn sctn = 0})"
apply (rule return_time_continuous_below)
apply (rule derivative_eq_intros refl)+
apply force
subgoal using ‹closed ivl› by auto
subgoal using prems pm by (auto simp: plane_of_def eventually_at_filter)
subgoal by (auto intro!: )
subgoal using prems pm by auto
subgoal using prems by auto
subgoal using prems pm by (auto intro!: assms simp: plane_of_def)
subgoal using prems pm by auto
done
then show "continuous (at x within below_halfspace sctn) (return_time {x ∈ ivl. x ∈ plane_of sctn})"
by (simp add: plane_of_def halfspace_simps)
qed
done
done
lemma do_intersection_spec_sctn_cong:
assumes "sctn = sctn' ∨ (normal sctn = - normal sctn' ∧ pstn sctn = - pstn sctn')"
shows "do_intersection_spec a b c sctn d e = do_intersection_spec a b c sctn' d e"
using assms
by (auto simp: do_intersection_spec_def plane_of_def set_eq_iff intro!: )
lemma poincare_onto_from[le, refine_vcg]:
assumes wd[refine_vcg]: "wd TYPE('a::enum rvec)"
assumes [refine_vcg]: "⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤ SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
assumes trapprop: "stable_on (Csafe - (ivl ∩ plane_of sctn)) trap"
shows "poincare_onto_from symstart trap S guards ivl sctn ro (XS0::'a eucl1 set) ≤
SPEC (poincare_mapsto (ivl ∩ plane_of sctn) (XS0 - trap × UNIV) S (Csafe - ivl ∩ plane_of sctn))"
unfolding poincare_onto_from_def autoref_tag_defs
apply (refine_vcg, clarsimp_all simp: trapprop)
subgoal by (auto simp: do_intersection_spec_def Int_def intro: poincare_mapsto_subset)
subgoal premises prems for a b c d e f
proof -
note prems
from trapprop
have stable: "stable_on (fst ` (e × UNIV ∩ sbelow_halfspace a × UNIV ∪ d)) trap"
apply (rule stable_on_mono)
using ‹fst ` (d ∪ e × UNIV) ⊆ Csafe› ‹a = sctn ∨ normal a = - normal sctn ∧ pstn a = - pstn sctn›
‹fst ` d ⊆ sbelow_halfspace a›
by (auto simp: halfspace_simps plane_of_def image_Un)
from prems(16) have "flowsto (XS0 - trap × UNIV) {0<..} (e × UNIV ∩ sbelow_halfspace a × UNIV) d"
by (rule flowsto_subset) auto
then have ft: "flowsto (XS0 - trap × UNIV) {0<..} ((e ∩ sbelow_halfspace a) × UNIV) (d - trap × UNIV)"
by (auto intro!: flowsto_mapsto_avoid_trap stable simp: Times_Int_distrib1)
from prems(8) have di: "do_intersection_spec UNIV {} ivl a (d - trap × UNIV) (f, Csafe - ivl ∩ plane_of sctn)"
apply (subst do_intersection_spec_sctn_cong)
defer apply assumption
using prems(2)
by auto
have "do_intersection_spec (below_halfspace a) {} ivl a (XS0 - trap × UNIV)
(f, e ∩ sbelow_halfspace a ∪ (Csafe - ivl ∩ plane_of sctn))"
apply (rule do_intersection_flowsto_trans_return[OF ft di])
subgoal using prems by (auto simp: do_intersection_spec_def halfspace_simps plane_of_def)
subgoal by (auto simp: halfspace_simps plane_of_def)
subgoal using prems by (auto simp: halfspace_simps plane_of_def)
subgoal using prems by (auto simp: do_intersection_spec_def halfspace_simps plane_of_def)
subgoal using prems by (auto simp: image_Un)
subgoal using prems by (auto simp: do_intersection_spec_def halfspace_simps plane_of_def)
subgoal using prems by (auto simp: do_intersection_spec_def halfspace_simps plane_of_def)
subgoal using prems by (auto simp: do_intersection_spec_def halfspace_simps plane_of_def)
done
moreover have "plane_of a = plane_of sctn"
using prems(2) by (auto simp: plane_of_def)
ultimately show ?thesis
apply (auto simp add: do_intersection_spec_def Int_def)
apply (rule poincare_mapsto_subset, assumption)
by auto
qed
done
lemma subset_spec1[refine_vcg]: "subset_spec1 R P dP ≤ SPEC (λb. b ⟶ R ⊆ flow1_of_vec1 ` (P × dP))"
unfolding subset_spec1_def
by refine_vcg (auto simp: vec1_of_flow1_def)
lemma subset_spec1_coll[le, refine_vcg]:
"subset_spec1_coll R P dP ≤ subset_spec R (flow1_of_vec1 ` (P × dP))"
unfolding autoref_tag_defs subset_spec_def subset_spec1_coll_def
by (refine_vcg) (auto simp: subset_iff set_of_ivl_def)
lemma one_step_until_time_spec[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "one_step_until_time (X0::'n eucl1 set) CX t1 ≤ SPEC (λ(R, CX).
(∀(x0, d0) ∈ X0. t1 ∈ existence_ivl0 x0 ∧
(flow0 x0 t1, Dflow x0 t1 o⇩L d0) ∈ R ∧
(∀t ∈ {0 .. t1}. flow0 x0 t ∈ CX)) ∧
fst ` R ∪ CX ⊆ Csafe)"
using [[simproc del: defined_all]]
unfolding one_step_until_time_def autoref_tag_defs
apply (refine_vcg WHILE_rule[where I="λ(t, h, X, CX). fst ` X ⊆ Csafe ∧ CX ⊆ Csafe ∧ 0 ≤ h ∧ 0 ≤ t ∧ t ≤ t1 ∧
(∀(x0, d0) ∈ X0. t ∈ existence_ivl0 x0 ∧
(flow0 x0 t, Dflow x0 t o⇩L d0) ∈ X ∧
(∀s ∈ {0 .. t}. flow0 x0 s ∈ CX))"])
subgoal by auto
subgoal by (force simp: flowpipe_def existence_ivl_trans flow_trans)
subgoal by (auto simp: flowpipe_def existence_ivl_trans flow_trans)
apply clarsimp subgoal for startstep rk2_param a b c d e f g h i j
apply (safe)
subgoal by (auto simp: flowpipe_def intro!: existence_ivl_trans flow_trans)
subgoal
apply (subst flow_trans, force)
subgoal by (auto simp: flowpipe_def intro!: existence_ivl_trans flow_trans)
apply (subst Dflow_trans, force)
subgoal by (auto simp: flowpipe_def intro!: existence_ivl_trans flow_trans)
by (auto simp: blinfun_compose_assoc flowpipe_def)
subgoal for s
apply (drule bspec[where x="(i, j)"], assumption)
apply auto
apply (cases "s ≤ a")
subgoal by auto
subgoal
apply (auto simp: blinfun_compose_assoc flowpipe_def)
apply (drule bspec, assumption)
apply auto
proof goal_cases
case 1
have a: "a ∈ existence_ivl0 i" using 1 by auto
have sa: "s - a ∈ existence_ivl0 (flow0 i a)"
using "1"(15) "1"(19) "1"(20) local.ivl_subset_existence_ivl by fastforce
have "flow0 i s = flow0 (flow0 i a) (s - a)"
by (auto simp: a sa flow_trans[symmetric])
also have "… ∈ f"
using 1 by auto
finally show ?case
using 1 by simp
qed
done
done
subgoal by auto
done
text ‹solve ODE until the time interval ‹{t1 .. t2}››
lemma ivl_of_eucl1_coll[THEN order_trans, refine_vcg]: "ivl_of_eucl_coll X ≤ SPEC (λR. X × UNIV ⊆ R)"
unfolding ivl_of_eucl_coll_def
by refine_vcg auto
lemma one_step_until_time_ivl_spec[le, refine_vcg]:
assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
shows "one_step_until_time_ivl (X0::'n eucl1 set) CX t1 t2 ≤ SPEC (λ(R, CX).
(∀(x0, d0) ∈ X0. {t1 .. t2} ⊆ existence_ivl0 x0 ∧
(∀t ∈ {t1 .. t2}. (flow0 x0 t, Dflow x0 t o⇩L d0) ∈ R) ∧
(∀t ∈ {0 .. t1}. (flow0 x0 t) ∈ CX)) ∧
fst ` R ∪ CX ⊆ Csafe)"
unfolding one_step_until_time_ivl_def
apply (refine_vcg, clarsimp_all)
subgoal for X CX Y CY CY' x0 d0
apply (drule bspec, assumption, clarsimp)
apply (drule bspec, assumption, clarsimp simp add: nonneg_interval_mem_existence_ivlI)
apply (rule subsetD, assumption)
subgoal for t
apply (drule bspec[where x=0], force)
apply (drule bspec[where x="t - t1"], force)
using interval_subset_existence_ivl[of t1 x0 t2]
by (auto simp: flow_trans')
done
done
lemma empty_symstart_flowsto:
"X0 ⊆ Csafe × UNIV ⟹
RETURN ({}, X0) ≤ SPEC (λ(CX, X). flowsto (X0 - {} × UNIV) {0..} (CX × UNIV) X)"
by (auto intro!: flowsto_self)
subsection ‹Poincare map returning to›
lemma poincare_onto_from_ivla[le, refine_vcg]:
assumes [refine_vcg]: "wd TYPE('n::enum rvec)"
assumes [refine_vcg]: "⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤ SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
assumes trapprop[refine_vcg]: "stable_on (Csafe - (ivl ∩ plane_of sctn)) trap"
shows "poincare_onto_from symstart trap S guards ivl sctn ro (XS0::'n eucl1 set) ≤ SPEC
(λP.
wd TYPE((real, 'n) vec) ∧
poincare_mapsto (ivl ∩ plane_of sctn) (XS0 - trap × UNIV) S (Csafe - ivl ∩ plane_of sctn) P)"
by (refine_vcg)
subsection ‹Poincare map onto (from outside of target)›
subsection ‹One step method (reachability in time)›
lemma c0_info_of_apprsI:
assumes "(b, a) ∈ clw_rel appr_rel"
assumes "x ∈ a"
shows "x ∈ c0_info_of_apprs b"
using assms
by (auto simp: appr_rel_br clw_rel_br c0_info_of_apprs_def c0_info_of_appr_def dest!: brD)
lemma c0_info_of_appr'I:
assumes "(b, a) ∈ ⟨clw_rel appr_rel⟩phantom_rel"
assumes "x ∈ a"
shows "x ∈ c0_info_of_appr' b"
using assms
by (auto simp add: c0_info_of_appr'_def intro!: c0_info_of_apprsI split: option.splits)
lemma poincare_onto_from_in_ivl[le, refine_vcg]:
assumes [refine_vcg]: "wd TYPE('n::enum rvec)"
assumes [refine_vcg]: "⋀X0. X0 ⊆ Csafe × UNIV ⟹ symstart X0 ≤ SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
assumes trapprop: "stable_on (Csafe - (ivl ∩ plane_of sctn)) trap"
shows "poincare_onto_from_in_ivl symstart trap S guards ivl sctn ro (XS0::'n::enum eucl1 set) P dP ≤
SPEC (λb. b ⟶ poincare_mapsto (ivl ∩ plane_of sctn) (XS0 - trap × UNIV) S (Csafe - ivl ∩ plane_of sctn) (flow1_of_vec1 ` (P × dP)))"
unfolding poincare_onto_from_in_ivl_def
apply (refine_vcg, clarsimp_all)
apply (rule trapprop)
apply (rule poincare_mapsto_subset)
apply assumption
by auto
lemma lvivl_default_relI:
"(dRi, set_of_lvivl' dRi::'e::executable_euclidean_space set) ∈ ⟨lvivl_rel⟩default_rel UNIV"
if "lvivl'_invar DIM('e) dRi"
using that
by (auto simp: set_of_lvivl'_def set_of_lvivl_def set_of_ivl_def lvivl'_invar_def
intro!: mem_default_relI lvivl_relI)
lemma stable_on_empty[simp]: "stable_on A {}"
by (auto simp: stable_on_def)
lemma poincare_onto_in_ivl[le, refine_vcg]:
assumes [simp]: "length (ode_e) = CARD('n::enum)"
shows "poincare_onto_in_ivl guards ivl sctn ro (XS0::'n::enum eucl1 set) P dP ≤
SPEC (λb. b ⟶ poincare_mapsto (ivl ∩ plane_of sctn) (XS0) UNIV (Csafe - ivl ∩ plane_of sctn) (flow1_of_vec1 ` (P × dP)))"
proof -
have wd[refine_vcg]: "wd TYPE((real, 'n) vec)" by (simp add: wd_def)
show ?thesis
unfolding poincare_onto_in_ivl_def
apply (refine_vcg)
subgoal by (auto intro!: flowsto_self)
subgoal
apply (clarsimp simp add: do_intersection_spec_def Int_def[symmetric])
apply (rule poincare_mapsto_subset)
apply assumption
by auto
done
qed
end
end