[STATEMENT]
lemma bouncing_ball_flow:
  fixes h::real
  assumes "g < 0" and "h \<ge> 0"
  shows "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
  \<lceil>\<lambda>s. s$1 = h \<and> s$2 = 0\<rceil> \<le> wp
    (LOOP
      ((x\<acute>= (\<lambda>t. f g) & (\<lambda> s. s$1 \<ge> 0) on (\<lambda>s. UNIV) UNIV @ 0);
      (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
    INV (\<lambda>s. 0 \<le> s$1 \<and> 2 * g * s$1 = 2 * g * h + s$2 * s$2))
  \<lceil>\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g < 0; 0 \<le> h\<rbrakk> \<Longrightarrow> \<lceil>\<lambda>s. s $ 1 = h \<and> s $ 2 = 0\<rceil> \<subseteq> wp (LOOP x\<acute>=\<lambda>t. f g & \<lambda>s. 0 \<le> s $ 1 on \<lambda>s. UNIV UNIV @ 0 ; (IF (\<lambda>s. s $ 1 = 0) THEN (2 ::= (\<lambda>s. - s $ 2)) ELSE skip) INV (\<lambda>s. 0 \<le> s $ 1 \<and> 2 \<cdot> g \<cdot> s $ 1 = 2 \<cdot> g \<cdot> h + s $ 2 \<cdot> s $ 2) ) \<lceil>\<lambda>s. 0 \<le> s $ 1 \<and> s $ 1 \<le> h\<rceil>
[PROOF STEP]
apply(rule wp_loopI, simp_all add: local_flow.wp_g_ode_subset[OF local_flow_ball])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g < 0; 0 \<le> h\<rbrakk> \<Longrightarrow> \<forall>s. 0 \<le> s $ 1 \<and> 2 \<cdot> g \<cdot> s $ 1 = 2 \<cdot> g \<cdot> h + s $ 2 \<cdot> s $ 2 \<longrightarrow> s $ 1 \<le> h
 2. \<lbrakk>g < 0; 0 \<le> h\<rbrakk> \<Longrightarrow> \<forall>s. 0 \<le> s $ 1 \<and> 2 \<cdot> g \<cdot> s $ 1 = 2 \<cdot> g \<cdot> h + s $ 2 \<cdot> s $ 2 \<longrightarrow> (\<forall>t. (\<forall>\<tau>\<le>t. 0 \<le> g \<cdot> \<tau>\<^sup>2 / 2 + s $ 2 \<cdot> \<tau> + s $ 1) \<longrightarrow> (g \<cdot> t\<^sup>2 / 2 + s $ 2 \<cdot> t + s $ 1 = 0 \<longrightarrow> 2 \<cdot> g \<cdot> h + (g \<cdot> t \<cdot> (g \<cdot> t + s $ 2) + s $ 2 \<cdot> (g \<cdot> t + s $ 2)) = 0) \<and> (g \<cdot> t\<^sup>2 / 2 + s $ 2 \<cdot> t + s $ 1 = 0 \<or> 2 \<cdot> g \<cdot> (g \<cdot> t\<^sup>2 / 2 + s $ 2 \<cdot> t + s $ 1) = 2 \<cdot> g \<cdot> h + (g \<cdot> t \<cdot> (g \<cdot> t + s $ 2) + s $ 2 \<cdot> (g \<cdot> t + s $ 2))))
[PROOF STEP]
by (auto simp: bb_real_arith)