[STATEMENT]
lemma bin_sign_mask [simp]: "bin_sign (mask n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_sign (mask n) = 0
[PROOF STEP]
by (simp add: bin_sign_def bin_mask_conv_pow2)


[STATEMENT]
lemma bin_mask_p1_conv_shift: "mask n + 1 = push_bit n (1 :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mask n + 1 = push_bit n 1
[PROOF STEP]
by (simp add: bin_mask_conv_pow2 shiftl_int_def)


[STATEMENT]
lemma sbintrunc_eq_in_range:
  "((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = x) = (x \<in> range ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n))"
  "(x = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x) = (x \<in> range ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (signed_take_bit n x = x) = (x \<in> range (signed_take_bit n)) &&& (x = signed_take_bit n x) = (x \<in> range (signed_take_bit n))
[PROOF STEP]
apply (simp_all add: image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (signed_take_bit n x = x) = (\<exists>xa. x = signed_take_bit n xa)
 2. (x = signed_take_bit n x) = (\<exists>xa. x = signed_take_bit n xa)
[PROOF STEP]
apply (metis sbintrunc_sbintrunc)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sbintrunc_If:
  "- 3 * (2 ^ n) \<le> x \<and> x < 3 * (2 ^ n)
    \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = (if x < - (2 ^ n) then x + 2 * (2 ^ n)
        else if x \<ge> 2 ^ n then x - 2 * (2 ^ n) else x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 3 * 2 ^ n \<le> x \<and> x < 3 * 2 ^ n \<Longrightarrow> signed_take_bit n x = (if x < - (2 ^ n) then x + 2 * 2 ^ n else if 2 ^ n \<le> x then x - 2 * 2 ^ n else x)
[PROOF STEP]
apply (simp add: no_sbintr_alt2, safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- (3 * 2 ^ n) \<le> x; x < 3 * 2 ^ n; 2 ^ n \<le> x\<rbrakk> \<Longrightarrow> 2 ^ n + (x + 2 ^ n) mod (2 * 2 ^ n) = x
 2. \<lbrakk>- (3 * 2 ^ n) \<le> x; x < 3 * 2 ^ n; \<not> 2 ^ n \<le> x; x < - (2 ^ n)\<rbrakk> \<Longrightarrow> (x + 2 ^ n) mod (2 * 2 ^ n) = 3 * 2 ^ n + x
[PROOF STEP]
apply (simp add: mod_pos_geq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- (3 * 2 ^ n) \<le> x; x < 3 * 2 ^ n; \<not> 2 ^ n \<le> x; x < - (2 ^ n)\<rbrakk> \<Longrightarrow> (x + 2 ^ n) mod (2 * 2 ^ n) = 3 * 2 ^ n + x
[PROOF STEP]
apply (subst mod_add_self1[symmetric], simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sint_range':
  \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint x \<and> sint x < 2 ^ (LENGTH('a) - Suc 0)\<close>
  for x :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint x \<and> sint x < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. - (2 ^ (LENGTH('a) - Suc 0)) \<le> signed_take_bit (LENGTH('a) - Suc 0) x \<and> signed_take_bit (LENGTH('a) - Suc 0) x < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
using sbintr_ge sbintr_lt
[PROOF STATE]
proof (prove)
using this:
- (2 ^ ?n) \<le> signed_take_bit ?n ?w
signed_take_bit ?n ?w < 2 ^ ?n

goal (1 subgoal):
 1. \<And>x. - (2 ^ (LENGTH('a) - Suc 0)) \<le> signed_take_bit (LENGTH('a) - Suc 0) x \<and> signed_take_bit (LENGTH('a) - Suc 0) x < 2 ^ (LENGTH('a) - Suc 0)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma signed_arith_eq_checks_to_ord:
  "(sint a + sint b = sint (a + b ))
    = ((a <=s a + b) = (0 <=s b))"
  "(sint a - sint b = sint (a - b ))
    = ((0 <=s a - b) = (b <=s a))"
  "(- sint a = sint (- a)) = (0 <=s (- a) = (a <=s 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sint a + sint b = sint (a + b)) = ((a \<le>s a + b) = (0 \<le>s b)) &&& (sint a - sint b = sint (a - b)) = ((0 \<le>s a - b) = (b \<le>s a)) &&& (- sint a = sint (- a)) = ((0 \<le>s - a) = (a \<le>s 0))
[PROOF STEP]
using sint_range'[where x=a] sint_range'[where x=b]
[PROOF STATE]
proof (prove)
using this:
- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint a \<and> sint a < 2 ^ (LENGTH('a) - Suc 0)
- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint b \<and> sint b < 2 ^ (LENGTH('a) - Suc 0)

goal (1 subgoal):
 1. (sint a + sint b = sint (a + b)) = ((a \<le>s a + b) = (0 \<le>s b)) &&& (sint a - sint b = sint (a - b)) = ((0 \<le>s a - b) = (b \<le>s a)) &&& (- sint a = sint (- a)) = ((0 \<le>s - a) = (a \<le>s 0))
[PROOF STEP]
by (simp_all add: sint_word_ariths word_sle_eq word_sless_alt sbintrunc_If)


[STATEMENT]
lemma signed_mult_eq_checks_double_size:
  assumes mult_le: "(2 ^ (len_of TYPE ('a) - 1) + 1) ^ 2 \<le> (2 :: int) ^ (len_of TYPE ('b) - 1)"
           and le: "2 ^ (LENGTH('a) - 1) \<le> (2 :: int) ^ (len_of TYPE ('b) - 1)"
  shows "(sint (a :: 'a :: len word) * sint b = sint (a * b))
       = (scast a * scast b = (scast (a * b) :: 'b :: len word))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
have P: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (size a - 1) (sint a * sint b) \<in> range ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (size a - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit (size a - 1) (sint a * sint b) \<in> range (signed_take_bit (size a - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
signed_take_bit (size a - 1) (sint a * sint b) \<in> range (signed_take_bit (size a - 1))

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
have abs: "!! x :: 'a word. abs (sint x) < 2 ^ (size a - 1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<bar>sint x\<bar> < 2 ^ (size a - 1) + 1
[PROOF STEP]
apply (cut_tac x=x in sint_range')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint x \<and> sint x < 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> \<bar>sint x\<bar> < 2 ^ (size a - 1) + 1
[PROOF STEP]
apply (simp add: abs_le_iff word_size)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<bar>sint ?x\<bar> < 2 ^ (size a - 1) + 1

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
have abs_ab: "abs (sint a * sint b) < 2 ^ (LENGTH('b) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>sint a * sint b\<bar> < 2 ^ (LENGTH('b) - 1)
[PROOF STEP]
using abs_mult_less[OF abs[where x=a] abs[where x=b]] mult_le
[PROOF STATE]
proof (prove)
using this:
\<bar>sint a\<bar> * \<bar>sint b\<bar> < (2 ^ (size a - 1) + 1) * (2 ^ (size a - 1) + 1)
(2 ^ (LENGTH('a) - 1) + 1)\<^sup>2 \<le> 2 ^ (LENGTH('b) - 1)

goal (1 subgoal):
 1. \<bar>sint a * sint b\<bar> < 2 ^ (LENGTH('b) - 1)
[PROOF STEP]
by (simp add: abs_mult power2_eq_square word_size)
[PROOF STATE]
proof (state)
this:
\<bar>sint a * sint b\<bar> < 2 ^ (LENGTH('b) - 1)

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
define r s where \<open>r = LENGTH('a) - 1\<close> \<open>s = LENGTH('b) - 1\<close>
[PROOF STATE]
proof (state)
this:
r = LENGTH('a) - 1
s = LENGTH('b) - 1

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = LENGTH('a) - 1
s = LENGTH('b) - 1
[PROOF STEP]
have \<open>LENGTH('a) = Suc r\<close> \<open>LENGTH('b) = Suc s\<close>
    \<open>size a = Suc r\<close> \<open>size b = Suc r\<close>
[PROOF STATE]
proof (prove)
using this:
r = LENGTH('a) - 1
s = LENGTH('b) - 1

goal (1 subgoal):
 1. (LENGTH('a) = Suc r &&& LENGTH('b) = Suc s) &&& size a = Suc r &&& size b = Suc r
[PROOF STEP]
by (simp_all add: word_size)
[PROOF STATE]
proof (state)
this:
LENGTH('a) = Suc r
LENGTH('b) = Suc s
size a = Suc r
size b = Suc r

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
LENGTH('a) = Suc r
LENGTH('b) = Suc s
size a = Suc r
size b = Suc r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
LENGTH('a) = Suc r
LENGTH('b) = Suc s
size a = Suc r
size b = Suc r

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
using P[unfolded range_sbintrunc] abs_ab le
[PROOF STATE]
proof (prove)
using this:
LENGTH('a) = Suc r
LENGTH('b) = Suc s
size a = Suc r
size b = Suc r
signed_take_bit (size a - 1) (sint a * sint b) \<in> {i. - (2 ^ (size a - 1)) \<le> i \<and> i < 2 ^ (size a - 1)}
\<bar>sint a * sint b\<bar> < 2 ^ (LENGTH('b) - 1)
2 ^ (LENGTH('a) - 1) \<le> 2 ^ (LENGTH('b) - 1)

goal (1 subgoal):
 1. (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LENGTH('a) = Suc r; LENGTH('b) = Suc s; size a = Suc r; size b = Suc r; \<bar>sint a * sint b\<bar> < 2 ^ s; r \<le> s\<rbrakk> \<Longrightarrow> (sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))
[PROOF STEP]
apply (transfer fixing: r s)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>LENGTH('a) = Suc r; LENGTH('b) = Suc s; LENGTH('a) = Suc r; LENGTH('a) = Suc r; \<bar>signed_take_bit (LENGTH('a) - Suc 0) a * signed_take_bit (LENGTH('a) - Suc 0) b\<bar> < 2 ^ s; r \<le> s\<rbrakk> \<Longrightarrow> (signed_take_bit (LENGTH('a) - Suc 0) a * signed_take_bit (LENGTH('a) - Suc 0) b = signed_take_bit (LENGTH('a) - Suc 0) (a * b)) = (take_bit LENGTH('b) (signed_take_bit (LENGTH('a) - Suc 0) a * signed_take_bit (LENGTH('a) - Suc 0) b) = take_bit LENGTH('b) (signed_take_bit (LENGTH('a) - Suc 0) (a * b)))
[PROOF STEP]
apply (auto simp add: signed_take_bit_int_eq_self simp flip: signed_take_bit_eq_iff_take_bit_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(sint a * sint b = sint (a * b)) = (scast a * scast b = scast (a * b))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bintrunc_id:
  "\<lbrakk>m \<le> int n; 0 < m\<rbrakk> \<Longrightarrow> take_bit n m = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> int n; 0 < m\<rbrakk> \<Longrightarrow> take_bit n m = m
[PROOF STEP]
by (simp add: take_bit_int_eq_self_iff le_less_trans)


[STATEMENT]
lemma bin_cat_cong: "concat_bit n b a = concat_bit m d c"
  if "n = m" "a = c" "take_bit m b = take_bit m d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat_bit n b a = concat_bit m d c
[PROOF STEP]
using that(3)
[PROOF STATE]
proof (prove)
using this:
take_bit m b = take_bit m d

goal (1 subgoal):
 1. concat_bit n b a = concat_bit m d c
[PROOF STEP]
unfolding that(1,2)
[PROOF STATE]
proof (prove)
using this:
take_bit m b = take_bit m d

goal (1 subgoal):
 1. concat_bit m b c = concat_bit m d c
[PROOF STEP]
by (simp add: bin_cat_eq_push_bit_add_take_bit)


[STATEMENT]
lemma bin_cat_eqD1: "concat_bit n b a = concat_bit n d c \<Longrightarrow> a = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat_bit n b a = concat_bit n d c \<Longrightarrow> a = c
[PROOF STEP]
by (metis drop_bit_bin_cat_eq)


[STATEMENT]
lemma bin_cat_eqD2: "concat_bit n b a = concat_bit n d c \<Longrightarrow> take_bit n b = take_bit n d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat_bit n b a = concat_bit n d c \<Longrightarrow> take_bit n b = take_bit n d
[PROOF STEP]
by (metis take_bit_bin_cat_eq)


[STATEMENT]
lemma bin_cat_inj: "(concat_bit n b a) = concat_bit n d c \<longleftrightarrow> a = c \<and> take_bit n b = take_bit n d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (concat_bit n b a = concat_bit n d c) = (a = c \<and> take_bit n b = take_bit n d)
[PROOF STEP]
by (auto intro: bin_cat_cong bin_cat_eqD1 bin_cat_eqD2)


[STATEMENT]
lemma bin_sc_pos:
  "0 \<le> i \<Longrightarrow> 0 \<le> bin_sc n b i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> i \<Longrightarrow> 0 \<le> set_bit_class.set_bit i n b
[PROOF STEP]
by (metis bin_sign_sc sign_Pls_ge_0)


[STATEMENT]
theorem T6: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
using F1
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. (((\<forall>x. x\<^bold>@w \<longrightarrow> \<G> x w \<longrightarrow> True) \<and> \<not> (\<forall>x. x\<^bold>@w \<longrightarrow> \<G> x w \<longrightarrow> False)) \<and> (\<forall>x xa. (\<forall>xa. (existsAt xa \<^bold>\<rightarrow> (\<G> xa \<^bold>\<rightarrow> x xa)) w) \<and> (\<forall>xb. (x xb \<^bold>\<rightarrow> xa xb) w) \<longrightarrow> (\<forall>x. (existsAt x \<^bold>\<rightarrow> (\<G> x \<^bold>\<rightarrow> xa x)) w))) \<and> (\<forall>x xa. (\<forall>xa. (existsAt xa \<^bold>\<rightarrow> (\<G> xa \<^bold>\<rightarrow> x xa)) w) \<and> (\<forall>x. (existsAt x \<^bold>\<rightarrow> (\<G> x \<^bold>\<rightarrow> xa x)) w) \<longrightarrow> (\<forall>xb. (existsAt xb \<^bold>\<rightarrow> (\<G> xb \<^bold>\<rightarrow> x\<^bold>\<sqinter>xa xb)) w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by auto \<comment>\<open>Proof found\<close>


[STATEMENT]
theorem T6again: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T3': "\<lfloor>\<^bold>\<exists>\<^sup>E \<G>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
using F1
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. (((\<forall>x. x\<^bold>@w \<longrightarrow> \<G> x w \<longrightarrow> True) \<and> \<not> (\<forall>x. x\<^bold>@w \<longrightarrow> \<G> x w \<longrightarrow> False)) \<and> (\<forall>x xa. (\<forall>xa. (existsAt xa \<^bold>\<rightarrow> (\<G> xa \<^bold>\<rightarrow> x xa)) w) \<and> (\<forall>xb. (x xb \<^bold>\<rightarrow> xa xb) w) \<longrightarrow> (\<forall>x. (existsAt x \<^bold>\<rightarrow> (\<G> x \<^bold>\<rightarrow> xa x)) w))) \<and> (\<forall>x xa. (\<forall>xa. (existsAt xa \<^bold>\<rightarrow> (\<G> xa \<^bold>\<rightarrow> x xa)) w) \<and> (\<forall>x. (existsAt x \<^bold>\<rightarrow> (\<G> x \<^bold>\<rightarrow> xa x)) w) \<longrightarrow> (\<forall>xb. (existsAt xb \<^bold>\<rightarrow> (\<G> xb \<^bold>\<rightarrow> x\<^bold>\<sqinter>xa xb)) w))\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T6:  "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
using T3'
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma T3: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
oops  \<comment>\<open>Countermodel\<close>


[STATEMENT]
lemma T3: assumes T: "\<lfloor>\<^bold>\<forall>\<phi>.((\<^bold>\<box>\<phi>) \<^bold>\<rightarrow> \<phi>)\<rfloor>"
          shows "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
using F1 T
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. (((\<forall>x. x\<^bold>@w \<longrightarrow> \<G> x w \<longrightarrow> True) \<and> \<not> (\<forall>x. x\<^bold>@w \<longrightarrow> \<G> x w \<longrightarrow> False)) \<and> (\<forall>x xa. (\<forall>xa. (existsAt xa \<^bold>\<rightarrow> (\<G> xa \<^bold>\<rightarrow> x xa)) w) \<and> (\<forall>xb. (x xb \<^bold>\<rightarrow> xa xb) w) \<longrightarrow> (\<forall>x. (existsAt x \<^bold>\<rightarrow> (\<G> x \<^bold>\<rightarrow> xa x)) w))) \<and> (\<forall>x xa. (\<forall>xa. (existsAt xa \<^bold>\<rightarrow> (\<G> xa \<^bold>\<rightarrow> x xa)) w) \<and> (\<forall>x. (existsAt x \<^bold>\<rightarrow> (\<G> x \<^bold>\<rightarrow> xa x)) w) \<longrightarrow> (\<forall>xb. (existsAt xb \<^bold>\<rightarrow> (\<G> xb \<^bold>\<rightarrow> x\<^bold>\<sqinter>xa xb)) w))\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. (\<^bold>\<box>x \<^bold>\<rightarrow> x) w\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by auto


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment>\<open>Consistency: model found\<close>


[STATEMENT]
lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w\<rfloor>
[PROOF STEP]
oops  \<comment>\<open>Countermodel\<close>


[STATEMENT]
lemma MT: "\<lfloor>\<^bold>\<forall>x y.(((\<G> x) \<^bold>\<and> (\<G> y)) \<^bold>\<rightarrow> (x\<^bold>=y))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x xa. (\<G> x \<^bold>\<and> \<G> xa) w \<longrightarrow> x = xa\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x xa. (\<G> x \<^bold>\<and> \<G> xa) w \<longrightarrow> x = xa\<rfloor>
[PROOF STEP]
oops \<comment>\<open>Countermodel\<close>


[STATEMENT]
lemma "fb\<^sub>\<F> F S = (\<Inter> \<circ> \<P> (- op\<^sub>K F)) (- S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> F S = (\<Inter> \<circ> \<P> (- op\<^sub>K F)) (- S)
[PROOF STEP]
unfolding ffb_def map_dual_def dual_set_def klift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>f. uminus \<circ> f \<circ> uminus) \<circ> (\<lambda>f. \<mu> \<circ> \<P> f) \<circ> op\<^sub>K) F S = (\<Inter> \<circ> \<P> (- op\<^sub>K F)) (- S)
[PROOF STEP]
by simp


[STATEMENT]
lemma "fb\<^sub>\<F> F S = {s. F s \<subseteq> S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> F S = {s. F s \<subseteq> S}
[PROOF STEP]
by (auto simp: ffb_def kop_def klift_def map_dual_def dual_set_def f2r_def r2f_def)


[STATEMENT]
lemma ffb_eq: "fb\<^sub>\<F> F S = {s. \<forall>s'. s' \<in> F s \<longrightarrow> s' \<in> S}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> F S = {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p S s'}
[PROOF STEP]
by (auto simp: ffb_def kop_def klift_def map_dual_def dual_set_def f2r_def r2f_def)


[STATEMENT]
lemma ffb_iso: "P \<le> Q \<Longrightarrow> fb\<^sub>\<F> F P \<le> fb\<^sub>\<F> F Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> Q \<Longrightarrow> fb\<^sub>\<F> F P \<subseteq> fb\<^sub>\<F> F Q
[PROOF STEP]
unfolding ffb_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> Q \<Longrightarrow> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p P s'} \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p Q s'}
[PROOF STEP]
by auto


[STATEMENT]
lemma ffb_invariants:
  assumes "{s. I s} \<le> fb\<^sub>\<F> F {s. I s}" and "{s. J s} \<le> fb\<^sub>\<F> F {s. J s}"
  shows "{s. I s \<and> J s} \<le> fb\<^sub>\<F> F {s. I s \<and> J s}"
    and "{s. I s \<or> J s} \<le> fb\<^sub>\<F> F {s. I s \<or> J s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. I s \<and> J s} \<subseteq> fb\<^sub>\<F> F {s. I s \<and> J s} &&& {s. I s \<or> J s} \<subseteq> fb\<^sub>\<F> F {s. I s \<or> J s}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{s. I s} \<subseteq> fb\<^sub>\<F> F {s. I s}
{s. J s} \<subseteq> fb\<^sub>\<F> F {s. J s}

goal (1 subgoal):
 1. {s. I s \<and> J s} \<subseteq> fb\<^sub>\<F> F {s. I s \<and> J s} &&& {s. I s \<or> J s} \<subseteq> fb\<^sub>\<F> F {s. I s \<or> J s}
[PROOF STEP]
unfolding ffb_eq
[PROOF STATE]
proof (prove)
using this:
{s. I s} \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p (Collect I) s'}
{s. J s} \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p (Collect J) s'}

goal (1 subgoal):
 1. {s. I s \<and> J s} \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p {s. I s \<and> J s} s'} &&& {s. I s \<or> J s} \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p {s. I s \<or> J s} s'}
[PROOF STEP]
by auto

\<comment> \<open> Skip \<close>


[STATEMENT]
lemma ffb_skip[simp]: "fb\<^sub>\<F> skip S = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> skip S = S
[PROOF STEP]
unfolding ffb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<partial>\<^sub>F \<circ> bd\<^sub>\<F> \<circ> op\<^sub>K) skip S = S
[PROOF STEP]
by(simp add: kop_def klift_def map_dual_def)

\<comment> \<open> Tests \<close>


[STATEMENT]
lemma ffb_test[simp]: "fb\<^sub>\<F> \<questiondown>P? Q = {s. P s \<longrightarrow> s \<in> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> \<questiondown>P? Q = {s. P s \<longrightarrow> s2p Q s}
[PROOF STEP]
unfolding ffb_eq test_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>s'. s2p {x. x = s \<and> P x} s' \<longrightarrow> s2p Q s'} = {s. P s \<longrightarrow> s2p Q s}
[PROOF STEP]
by simp

\<comment> \<open> Assignments \<close>


[STATEMENT]
lemma ffb_assign[simp]: "fb\<^sub>\<F> (x ::= e) Q = {s. (\<chi> j. ((($) s)(x := (e s))) j) \<in> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> (x ::= e) Q = {s. s2p Q (\<chi>j. ((($) s)(x := e s)) j)}
[PROOF STEP]
unfolding vec_upd_def assign_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> (\<lambda>s. skip (vec_lambda ((($) s)(x := e s)))) Q = {s. s2p Q (\<chi>j. ((($) s)(x := e s)) j)}
[PROOF STEP]
by (subst ffb_eq) simp

\<comment> \<open> Nondeterministic assignments \<close>


[STATEMENT]
lemma fbox_nondet_assign[simp]: "fb\<^sub>\<F> (x ::= ?) P = {s. \<forall>k. (\<chi> j. if j = x then k else s$j) \<in> P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> (x ::= ? ) P = {s. \<forall>k. s2p P (\<chi>j. if j = x then k else s $ j)}
[PROOF STEP]
unfolding ffb_eq nondet_assign_def vec_upd_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>s'. s2p {\<chi>j. if j = x then k else s $ j |k. True} s' \<longrightarrow> s2p P s'} = {s. \<forall>k. s2p P (\<chi>j. if j = x then k else s $ j)}
[PROOF STEP]
apply(simp add: fun_eq_iff, safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa k. \<forall>s'. (\<exists>k. s' = (\<chi>j. if j = x then k else xa $ j)) \<longrightarrow> s2p P s' \<Longrightarrow> s2p P (\<chi>j. if j = x then k else xa $ j)
 2. \<And>xa s' k. \<forall>k. s2p P (\<chi>j. if j = x then k else xa $ j) \<Longrightarrow> s2p P (\<chi>j. if j = x then k else xa $ j)
[PROOF STEP]
by (erule_tac x="(\<chi> j. if j = x then k else _ $ j)" in allE, auto)

\<comment> \<open> Nondeterministic choice \<close>


[STATEMENT]
lemma ffb_choice: "fb\<^sub>\<F> (\<lambda>s. F s \<union> G s) P = fb\<^sub>\<F> F P \<inter> fb\<^sub>\<F> G P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> (\<lambda>s. F s \<union> G s) P = fb\<^sub>\<F> F P \<inter> fb\<^sub>\<F> G P
[PROOF STEP]
unfolding ffb_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>s'. s2p (F s \<union> G s) s' \<longrightarrow> s2p P s'} = {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p P s'} \<inter> {s. \<forall>s'. s2p (G s) s' \<longrightarrow> s2p P s'}
[PROOF STEP]
by auto


[STATEMENT]
lemma le_ffb_choice_iff: "P \<subseteq> fb\<^sub>\<F> (\<lambda>s. F s \<union> G s) Q \<longleftrightarrow> P \<subseteq> fb\<^sub>\<F> F Q \<and> P \<subseteq> fb\<^sub>\<F> G Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<subseteq> fb\<^sub>\<F> (\<lambda>s. F s \<union> G s) Q) = (P \<subseteq> fb\<^sub>\<F> F Q \<and> P \<subseteq> fb\<^sub>\<F> G Q)
[PROOF STEP]
unfolding ffb_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<subseteq> {s. \<forall>s'. s2p (F s \<union> G s) s' \<longrightarrow> s2p Q s'}) = (P \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p Q s'} \<and> P \<subseteq> {s. \<forall>s'. s2p (G s) s' \<longrightarrow> s2p Q s'})
[PROOF STEP]
by auto

\<comment> \<open> Sequential composition \<close>


[STATEMENT]
lemma ffb_kcomp[simp]: "fb\<^sub>\<F> (G ; F) P = fb\<^sub>\<F> G (fb\<^sub>\<F> F P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> (G ; F) P = fb\<^sub>\<F> G (fb\<^sub>\<F> F P)
[PROOF STEP]
unfolding ffb_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>s'. s2p ((G ; F) s) s' \<longrightarrow> s2p P s'} = {s. \<forall>s'. s2p (G s) s' \<longrightarrow> s2p {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p P s'} s'}
[PROOF STEP]
by (auto simp: kcomp_def)


[STATEMENT]
lemma hoare_kcomp:
  assumes "P \<le> fb\<^sub>\<F> F R" "R \<le> fb\<^sub>\<F> G Q"
  shows "P \<le> fb\<^sub>\<F> (F ; G) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (F ; G) Q
[PROOF STEP]
apply(subst ffb_kcomp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> F (fb\<^sub>\<F> G Q)
[PROOF STEP]
by (rule order.trans[OF assms(1)]) (rule ffb_iso[OF assms(2)])

\<comment> \<open> Conditional statement \<close>


[STATEMENT]
lemma ffb_if_then_else[simp]:
  "fb\<^sub>\<F> (IF T THEN X ELSE Y) Q = {s. T s \<longrightarrow> s \<in> fb\<^sub>\<F> X Q} \<inter> {s. \<not> T s \<longrightarrow> s \<in> fb\<^sub>\<F> Y Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> (IF T THEN X ELSE Y) Q = {s. T s \<longrightarrow> s2p (fb\<^sub>\<F> X Q) s} \<inter> {s. \<not> T s \<longrightarrow> s2p (fb\<^sub>\<F> Y Q) s}
[PROOF STEP]
unfolding ffb_eq ifthenelse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>s'. s2p (if T s then X s else Y s) s' \<longrightarrow> s2p Q s'} = {s. T s \<longrightarrow> s2p {s. \<forall>s'. s2p (X s) s' \<longrightarrow> s2p Q s'} s} \<inter> {s. \<not> T s \<longrightarrow> s2p {s. \<forall>s'. s2p (Y s) s' \<longrightarrow> s2p Q s'} s}
[PROOF STEP]
by auto


[STATEMENT]
lemma hoare_if_then_else:
  assumes "P \<inter> {s. T s} \<le> fb\<^sub>\<F> X Q"
    and "P \<inter> {s. \<not> T s} \<le> fb\<^sub>\<F> Y Q"
  shows "P \<le> fb\<^sub>\<F> (IF T THEN X ELSE Y) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (IF T THEN X ELSE Y) Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<inter> {s. T s} \<subseteq> fb\<^sub>\<F> X Q
P \<inter> {s. \<not> T s} \<subseteq> fb\<^sub>\<F> Y Q

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (IF T THEN X ELSE Y) Q
[PROOF STEP]
apply(subst ffb_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<inter> {s. T s} \<subseteq> fb\<^sub>\<F> X Q; P \<inter> {s. \<not> T s} \<subseteq> fb\<^sub>\<F> Y Q\<rbrakk> \<Longrightarrow> P \<subseteq> {s. \<forall>s'. s2p ((IF T THEN X ELSE Y) s) s' \<longrightarrow> s2p Q s'}
[PROOF STEP]
apply(subst (asm) ffb_eq)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<inter> Collect T \<subseteq> {s. \<forall>s'. s2p (X s) s' \<longrightarrow> s2p Q s'}; P \<inter> {s. \<not> T s} \<subseteq> {s. \<forall>s'. s2p (Y s) s' \<longrightarrow> s2p Q s'}\<rbrakk> \<Longrightarrow> P \<subseteq> {s. \<forall>s'. s2p ((IF T THEN X ELSE Y) s) s' \<longrightarrow> s2p Q s'}
[PROOF STEP]
unfolding ifthenelse_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<inter> Collect T \<subseteq> {s. \<forall>s'. s2p (X s) s' \<longrightarrow> s2p Q s'}; P \<inter> {s. \<not> T s} \<subseteq> {s. \<forall>s'. s2p (Y s) s' \<longrightarrow> s2p Q s'}\<rbrakk> \<Longrightarrow> P \<subseteq> {s. \<forall>s'. s2p (if T s then X s else Y s) s' \<longrightarrow> s2p Q s'}
[PROOF STEP]
by auto

\<comment> \<open> Finite iteration \<close>


[STATEMENT]
lemma kpower_inv: "I \<le> {s. \<forall>y. y \<in> F s \<longrightarrow> y \<in> I} \<Longrightarrow> I \<le> {s. \<forall>y. y \<in> (kpower F n s) \<longrightarrow> y \<in> I}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> {s. \<forall>y. s2p (F s) y \<longrightarrow> s2p I y} \<Longrightarrow> I \<subseteq> {s. \<forall>y. s2p (kpower F n s) y \<longrightarrow> s2p I y}
[PROOF STEP]
apply(induct n, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>I \<subseteq> {s. \<forall>y. s2p (F s) y \<longrightarrow> s2p I y} \<Longrightarrow> I \<subseteq> {s. \<forall>y. s2p (kpower F n s) y \<longrightarrow> s2p I y}; I \<subseteq> {s. \<forall>y. s2p (F s) y \<longrightarrow> s2p I y}\<rbrakk> \<Longrightarrow> I \<subseteq> {s. \<forall>y. s2p (kpower F (Suc n) s) y \<longrightarrow> s2p I y}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>I \<subseteq> {s. \<forall>y. s2p (kpower F n s) y \<longrightarrow> s2p I y}; I \<subseteq> {s. \<forall>y. s2p (F s) y \<longrightarrow> s2p I y}\<rbrakk> \<Longrightarrow> I \<subseteq> {s. \<forall>y. s2p ((F ; kpower F n) s) y \<longrightarrow> s2p I y}
[PROOF STEP]
by(auto simp: kcomp_prop)


[STATEMENT]
lemma kstar_inv: "I \<le> fb\<^sub>\<F> F I \<Longrightarrow> I \<subseteq> fb\<^sub>\<F> (kstar F) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> fb\<^sub>\<F> F I \<Longrightarrow> I \<subseteq> fb\<^sub>\<F> (kstar F) I
[PROOF STEP]
unfolding kstar_def ffb_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p I s'} \<Longrightarrow> I \<subseteq> {s. \<forall>s'. s2p ((\<Squnion> range (kpower F)) s) s' \<longrightarrow> s2p I s'}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x s' xa. \<lbrakk>I \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p I s'}; s2p I x; s2p (kpower F xa x) s'\<rbrakk> \<Longrightarrow> s2p I s'
[PROOF STEP]
using kpower_inv
[PROOF STATE]
proof (prove)
using this:
?I \<subseteq> {s. \<forall>y. s2p (?F s) y \<longrightarrow> s2p ?I y} \<Longrightarrow> ?I \<subseteq> {s. \<forall>y. s2p (kpower ?F ?n s) y \<longrightarrow> s2p ?I y}

goal (1 subgoal):
 1. \<And>x s' xa. \<lbrakk>I \<subseteq> {s. \<forall>s'. s2p (F s) s' \<longrightarrow> s2p I s'}; s2p I x; s2p (kpower F xa x) s'\<rbrakk> \<Longrightarrow> s2p I s'
[PROOF STEP]
by blast


[STATEMENT]
lemma ffb_kstarI:
  assumes "P \<le> I" and "I \<le> Q" and "I \<le> fb\<^sub>\<F> F I"
  shows "P \<le> fb\<^sub>\<F> (kstar F) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
have "I \<subseteq> fb\<^sub>\<F> (kstar F) I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> fb\<^sub>\<F> (kstar F) I
[PROOF STEP]
using assms(3) kstar_inv
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> fb\<^sub>\<F> F I
?I \<subseteq> fb\<^sub>\<F> ?F ?I \<Longrightarrow> ?I \<subseteq> fb\<^sub>\<F> (kstar ?F) ?I

goal (1 subgoal):
 1. I \<subseteq> fb\<^sub>\<F> (kstar F) I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I \<subseteq> fb\<^sub>\<F> (kstar F) I

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
hence "P \<le> fb\<^sub>\<F> (kstar F) I"
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> fb\<^sub>\<F> (kstar F) I

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) I
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> fb\<^sub>\<F> (kstar F) I
P \<subseteq> I

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<subseteq> fb\<^sub>\<F> (kstar F) I

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P \<subseteq> fb\<^sub>\<F> (kstar F) I

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
have "fb\<^sub>\<F> (kstar F) I \<le> fb\<^sub>\<F> (kstar F) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> (kstar F) I \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
by (rule ffb_iso[OF assms(2)])
[PROOF STATE]
proof (state)
this:
fb\<^sub>\<F> (kstar F) I \<subseteq> fb\<^sub>\<F> (kstar F) Q

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> fb\<^sub>\<F> (kstar F) Q

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P \<subseteq> fb\<^sub>\<F> (kstar F) Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma change_loopI: "LOOP X INV G = LOOP X INV I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LOOP X INV G  = LOOP X INV I
[PROOF STEP]
unfolding loopi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kstar X = kstar X
[PROOF STEP]
by simp


[STATEMENT]
lemma ffb_loopI: "P \<le> {s. I s}  \<Longrightarrow> {s. I s} \<le> Q \<Longrightarrow> {s. I s} \<le> fb\<^sub>\<F> F {s. I s} \<Longrightarrow> P \<le> fb\<^sub>\<F> (LOOP F INV I) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq> {s. I s}; {s. I s} \<subseteq> Q; {s. I s} \<subseteq> fb\<^sub>\<F> F {s. I s}\<rbrakk> \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> (LOOP F INV I ) Q
[PROOF STEP]
unfolding loopi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq> {s. I s}; {s. I s} \<subseteq> Q; {s. I s} \<subseteq> fb\<^sub>\<F> F {s. I s}\<rbrakk> \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
using ffb_kstarI[of "P"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P \<subseteq> ?I; ?I \<subseteq> ?Q; ?I \<subseteq> fb\<^sub>\<F> ?F ?I\<rbrakk> \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> (kstar ?F) ?Q

goal (1 subgoal):
 1. \<lbrakk>P \<subseteq> {s. I s}; {s. I s} \<subseteq> Q; {s. I s} \<subseteq> fb\<^sub>\<F> F {s. I s}\<rbrakk> \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> (kstar F) Q
[PROOF STEP]
by simp


[STATEMENT]
lemma ffb_loopI_break:
  "P \<le> fb\<^sub>\<F> Y {s. I s} \<Longrightarrow> {s. I s} \<le> fb\<^sub>\<F> X {s. I s} \<Longrightarrow> {s. I s} \<le> Q \<Longrightarrow> P \<le> fb\<^sub>\<F> (Y ; (LOOP X INV I)) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq> fb\<^sub>\<F> Y {s. I s}; {s. I s} \<subseteq> fb\<^sub>\<F> X {s. I s}; {s. I s} \<subseteq> Q\<rbrakk> \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> (Y ; (LOOP X INV I )) Q
[PROOF STEP]
by (rule hoare_kcomp, force) (rule ffb_loopI, auto)


[STATEMENT]
lemma fbox_g_evol[simp]:
  fixes \<phi> :: "('a::preorder) \<Rightarrow> 'b \<Rightarrow> 'b"
  shows "fb\<^sub>\<F> (EVOL \<phi> G U) Q = {s. (\<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (\<phi> \<tau> s)) \<longrightarrow> (\<phi> t s) \<in> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> (EVOL \<phi> G U) Q = {s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s)}
[PROOF STEP]
unfolding g_evol_def g_orbit_eq ffb_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>s'. s2p {\<phi> t s |t. s2p (U s) t \<and> (\<forall>\<tau>\<in>down (U s) t. G (\<phi> \<tau> s))} s' \<longrightarrow> s2p Q s'} = {s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s)}
[PROOF STEP]
by auto


[STATEMENT]
lemma ffb_g_orbital: "fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) Q =
  {s. \<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> (X t) \<in> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q = {s. \<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> s2p Q (X t)}
[PROOF STEP]
unfolding ffb_eq g_orbital_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>s'. s2p {X t |t X. s2p (U s) t \<and> \<P> X (down (U s) t) \<subseteq> Collect G \<and> s2p (Sols f U S t\<^sub>0 s) X} s' \<longrightarrow> s2p Q s'} = {s. \<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> s2p Q (X t)}
[PROOF STEP]
by (auto simp: fun_eq_iff)


[STATEMENT]
lemma ffb_g_ode_subset:
  assumes "\<And>s. s \<in> S \<Longrightarrow> 0 \<in> U s \<and> is_interval (U s) \<and> U s \<subseteq> T"
  shows "fb\<^sub>\<F> (x\<acute>= (\<lambda>t. f) & G on U S @ 0) Q =
  {s. s \<in> S \<longrightarrow> (\<forall>t\<in>(U s). (\<forall>\<tau>\<in>down (U s) t. G (\<phi> \<tau> s)) \<longrightarrow> (\<phi> t s) \<in> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on U S @ 0 Q = {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s))}
[PROOF STEP]
apply(unfold ffb_g_orbital set_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. s2p {s. \<forall>X\<in>Sols (\<lambda>t. f) U S 0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> s2p Q (X t)} x = s2p {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s))} x
[PROOF STEP]
apply(clarify, rule iffI; clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x t. \<lbrakk>\<forall>X\<in>Sols (\<lambda>t. f) U S 0 x. \<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (X \<tau>)) \<longrightarrow> s2p Q (X t); s2p S x; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)\<rbrakk> \<Longrightarrow> s2p Q (\<phi> t x)
 2. \<And>x X t. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>)\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
apply(force simp: in_ivp_sols assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x X t. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>)\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
apply(frule ivp_solsD(2), frule ivp_solsD(3), frule ivp_solsD(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x X t. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
apply(subgoal_tac "\<forall>\<tau>\<in>down (U x) t. X \<tau> = \<phi> \<tau> x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x X t. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; \<forall>\<tau>\<in>down (U x) t. X \<tau> = \<phi> \<tau> x\<rbrakk> \<Longrightarrow> s2p Q (X t)
 2. \<And>x X t. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0\<rbrakk> \<Longrightarrow> \<forall>\<tau>\<in>down (U x) t. X \<tau> = \<phi> \<tau> x
[PROOF STEP]
apply(clarsimp, fastforce, rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> X \<tau> = \<phi> \<tau> x
[PROOF STEP]
apply(rule ivp_unique_solution[OF _ _ _ _ _ in_ivp_sols])
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p S x
 2. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> is_interval (?U63 x X t \<tau> x)
 3. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> ?U63 x X t \<tau> x \<subseteq> T
 4. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p (?U63 x X t \<tau> x) \<tau>
 5. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p (Sols (\<lambda>t. f) (?U63 x X t \<tau>) S 0 x) X
 6. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p S x
 7. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p (?U63 x X t \<tau> x) 0
 8. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> ?U63 x X t \<tau> x \<subseteq> T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s2p S ?s \<Longrightarrow> s2p (U ?s) 0 \<and> is_interval (U ?s) \<and> U ?s \<subseteq> T

goal (8 subgoals):
 1. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p S x
 2. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> is_interval (?U63 x X t \<tau> x)
 3. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> ?U63 x X t \<tau> x \<subseteq> T
 4. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p (?U63 x X t \<tau> x) \<tau>
 5. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p (Sols (\<lambda>t. f) (?U63 x X t \<tau>) S 0 x) X
 6. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p S x
 7. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> s2p (?U63 x X t \<tau> x) 0
 8. \<And>x X t \<tau>. \<lbrakk>s2p S x \<longrightarrow> (\<forall>t\<in>U x. (\<forall>\<tau>\<in>down (U x) t. G (\<phi> \<tau> x)) \<longrightarrow> s2p Q (\<phi> t x)); s2p (Sols (\<lambda>t. f) U S 0 x) X; s2p (U x) t; \<forall>\<tau>\<in>down (U x) t. G (X \<tau>); X 0 = x; s2p (U x \<rightarrow> S) X; s2p (U x) 0; s2p (down (U x) t) \<tau>\<rbrakk> \<Longrightarrow> ?U63 x X t \<tau> x \<subseteq> T
[PROOF STEP]
by auto


[STATEMENT]
lemma ffb_g_ode: "fb\<^sub>\<F> (x\<acute>= (\<lambda>t. f) & G on (\<lambda>s. T) S @ 0) Q =
  {s. s \<in> S \<longrightarrow> (\<forall>t\<in>T. (\<forall>\<tau>\<in>down T t. G (\<phi> \<tau> s)) \<longrightarrow> (\<phi> t s) \<in> Q)}" (is "_ = ?wlp")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on \<lambda>s. T S @ 0 Q = {s. s2p S s \<longrightarrow> (\<forall>t\<in>T. (\<forall>\<tau>\<in>down T t. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s))}
[PROOF STEP]
by (subst ffb_g_ode_subset, simp_all add: init_time interval_time)


[STATEMENT]
lemma ffb_g_ode_ivl: "t \<ge> 0 \<Longrightarrow> t \<in> T \<Longrightarrow> fb\<^sub>\<F> (x\<acute>=(\<lambda>t. f) & G on (\<lambda>s. {0..t}) S @ 0) Q =
  {s. s \<in> S \<longrightarrow> (\<forall>t\<in>{0..t}. (\<forall>\<tau>\<in>{0..t}. G (\<phi> \<tau> s)) \<longrightarrow> (\<phi> t s) \<in> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> t; s2p T t\<rbrakk> \<Longrightarrow> fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on \<lambda>s. {0..t} S @ 0 Q = {s. s2p S s \<longrightarrow> (\<forall>t\<in>{0..t}. (\<forall>\<tau>\<in>{0..t}. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s))}
[PROOF STEP]
apply(subst ffb_g_ode_subset, simp_all add: subintervalI init_time real_Icc_closed_segment)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> t; s2p T t\<rbrakk> \<Longrightarrow> {s. s2p S s \<longrightarrow> (\<forall>ta\<in>{0--t}. (\<forall>\<tau>. s2p {0--t} \<tau> \<and> \<tau> \<le> ta \<longrightarrow> G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> ta s))} = {s. s2p S s \<longrightarrow> (\<forall>t\<in>{0--t}. (\<forall>\<tau>\<in>{0..t}. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s))}
[PROOF STEP]
by (auto simp: closed_segment_eq_real_ivl)


[STATEMENT]
lemma ffb_orbit: "fb\<^sub>\<F> \<gamma>\<^sup>\<phi> Q = {s. s \<in> S \<longrightarrow> (\<forall> t \<in> T. \<phi> t s \<in> Q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> \<gamma>\<^sup>\<phi> Q = {s. s2p S s \<longrightarrow> (\<forall>t\<in>T. s2p Q (\<phi> t s))}
[PROOF STEP]
unfolding orbit_def ffb_g_ode
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. s2p S s \<longrightarrow> (\<forall>t\<in>T. (\<forall>\<tau>\<in>down T t. True) \<longrightarrow> s2p Q (\<phi> t s))} = {s. s2p S s \<longrightarrow> (\<forall>t\<in>T. s2p Q (\<phi> t s))}
[PROOF STEP]
by simp


[STATEMENT]
lemma ffb_g_orbital_guard:
  assumes "H = (\<lambda>s. G s \<and> Q s)"
  shows "fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. Q s} = fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. H s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. Q s} = fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. H s}
[PROOF STEP]
unfolding ffb_g_orbital
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> s2p (Collect Q) (X t)} = {s. \<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> s2p (Collect H) (X t)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
H = (\<lambda>s. G s \<and> Q s)

goal (1 subgoal):
 1. {s. \<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> s2p (Collect Q) (X t)} = {s. \<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> s2p (Collect H) (X t)}
[PROOF STEP]
by auto


[STATEMENT]
lemma ffb_g_orbital_inv:
  assumes "P \<le> I" and "I \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) I" and "I \<le> Q"
  shows "P \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> I

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
apply(rule order.trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. I \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 I

goal (1 subgoal):
 1. I \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
apply(rule order.trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 I \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
by (rule ffb_iso[OF assms(3)])


[STATEMENT]
lemma ffb_diff_inv[simp]:
  "({s. I s} \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. I s}) = diff_invariant I f U S t\<^sub>0 G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}) = diff_invariant I f U S t\<^sub>0 G
[PROOF STEP]
by (auto simp: diff_invariant_def ivp_sols_def ffb_eq g_orbital_eq)


[STATEMENT]
lemma bdf_diff_inv:
  "diff_invariant I f U S t\<^sub>0 G = (bd\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. I s} \<le> {s. I s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_invariant I f U S t\<^sub>0 G = (bd\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s} \<subseteq> {s. I s})
[PROOF STEP]
unfolding ffb_fbd_galois_var
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_invariant I f U S t\<^sub>0 G = (Collect I \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 (Collect I))
[PROOF STEP]
by (auto simp: diff_invariant_def ivp_sols_def ffb_eq g_orbital_eq)


[STATEMENT]
lemma diff_inv_guard_ignore:
  assumes "{s. I s} \<le> fb\<^sub>\<F> (x\<acute>= f & (\<lambda>s. True) on U S @ t\<^sub>0) {s. I s}"
  shows "{s. I s} \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. I s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & \<lambda>s. True on U S @ t\<^sub>0 {s. I s}

goal (1 subgoal):
 1. {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}
[PROOF STEP]
unfolding ffb_diff_inv diff_invariant_eq image_le_pred
[PROOF STATE]
proof (prove)
using this:
\<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. True) \<longrightarrow> I (X t))

goal (1 subgoal):
 1. \<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols f U S t\<^sub>0 s. \<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. G (X \<tau>)) \<longrightarrow> I (X t))
[PROOF STEP]
by auto


[STATEMENT]
lemma ffb_diff_inv_eq:
  assumes "\<And>s. s \<in> S \<Longrightarrow> 0 \<in> U s \<and> is_interval (U s) \<and> U s \<subseteq> T"
  shows "diff_invariant I (\<lambda>t. f) U S 0 (\<lambda>s. True) =
  ({s. s \<in> S \<longrightarrow> I s} = fb\<^sub>\<F> (x\<acute>= (\<lambda>t. f) & (\<lambda>s. True) on U S @ 0) {s. s \<in> S \<longrightarrow> I s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_invariant I (\<lambda>t. f) U S 0 (\<lambda>s. True) = ({s. s2p S s \<longrightarrow> I s} = fb\<^sub>\<F> x\<acute>=\<lambda>t. f & \<lambda>s. True on U S @ 0 {s. s2p S s \<longrightarrow> I s})
[PROOF STEP]
unfolding ffb_diff_inv[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Collect I \<subseteq> fb\<^sub>\<F> x\<acute>=\<lambda>t. f & \<lambda>s. True on U S @ 0 (Collect I)) = ({s. s2p S s \<longrightarrow> I s} = fb\<^sub>\<F> x\<acute>=\<lambda>t. f & \<lambda>s. True on U S @ 0 {s. s2p S s \<longrightarrow> I s})
[PROOF STEP]
apply(subst ffb_g_ode_subset[OF assms], simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Collect I \<subseteq> {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. True) \<longrightarrow> s2p (Collect I) (\<phi> t s))}) = ({s. s2p S s \<longrightarrow> I s} = {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. (\<forall>\<tau>\<in>down (U s) t. True) \<longrightarrow> s2p {s. s2p S s \<longrightarrow> I s} (\<phi> t s))})
[PROOF STEP]
apply(clarsimp simp: set_eq_iff, safe, force)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>Collect I \<subseteq> {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. I (\<phi> t s))}; s2p S x; \<forall>t\<in>U x. s2p S (\<phi> t x) \<longrightarrow> I (\<phi> t x)\<rbrakk> \<Longrightarrow> I x
 2. \<And>x t. \<lbrakk>\<forall>x. (s2p S x \<longrightarrow> I x) = (s2p S x \<longrightarrow> (\<forall>t\<in>U x. s2p S (\<phi> t x) \<longrightarrow> I (\<phi> t x))); I x; s2p S x; s2p (U x) t\<rbrakk> \<Longrightarrow> I (\<phi> t x)
[PROOF STEP]
apply(erule_tac x=0 in ballE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>Collect I \<subseteq> {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. I (\<phi> t s))}; s2p S x; s2p S (\<phi> 0 x) \<longrightarrow> I (\<phi> 0 x)\<rbrakk> \<Longrightarrow> I x
 2. \<And>x. \<lbrakk>Collect I \<subseteq> {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. I (\<phi> t s))}; s2p S x; 0 \<notin> U x\<rbrakk> \<Longrightarrow> I x
 3. \<And>x t. \<lbrakk>\<forall>x. (s2p S x \<longrightarrow> I x) = (s2p S x \<longrightarrow> (\<forall>t\<in>U x. s2p S (\<phi> t x) \<longrightarrow> I (\<phi> t x))); I x; s2p S x; s2p (U x) t\<rbrakk> \<Longrightarrow> I (\<phi> t x)
[PROOF STEP]
using init_time in_domain ivp(2) assms
[PROOF STATE]
proof (prove)
using this:
s2p T 0
s2p S ?s \<Longrightarrow> s2p (T \<rightarrow> S) (\<lambda>t. \<phi> t ?s)
s2p S ?s \<Longrightarrow> \<phi> 0 ?s = ?s
s2p S ?s \<Longrightarrow> s2p (U ?s) 0 \<and> is_interval (U ?s) \<and> U ?s \<subseteq> T

goal (3 subgoals):
 1. \<And>x. \<lbrakk>Collect I \<subseteq> {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. I (\<phi> t s))}; s2p S x; s2p S (\<phi> 0 x) \<longrightarrow> I (\<phi> 0 x)\<rbrakk> \<Longrightarrow> I x
 2. \<And>x. \<lbrakk>Collect I \<subseteq> {s. s2p S s \<longrightarrow> (\<forall>t\<in>U s. I (\<phi> t s))}; s2p S x; 0 \<notin> U x\<rbrakk> \<Longrightarrow> I x
 3. \<And>x t. \<lbrakk>\<forall>x. (s2p S x \<longrightarrow> I x) = (s2p S x \<longrightarrow> (\<forall>t\<in>U x. s2p S (\<phi> t x) \<longrightarrow> I (\<phi> t x))); I x; s2p S x; s2p (U x) t\<rbrakk> \<Longrightarrow> I (\<phi> t x)
[PROOF STEP]
apply(force, force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>\<forall>x. (s2p S x \<longrightarrow> I x) = (s2p S x \<longrightarrow> (\<forall>t\<in>U x. s2p S (\<phi> t x) \<longrightarrow> I (\<phi> t x))); I x; s2p S x; s2p (U x) t\<rbrakk> \<Longrightarrow> I (\<phi> t x)
[PROOF STEP]
apply(erule_tac x=x in allE, clarsimp, erule_tac x=t in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x t. \<lbrakk>I x; s2p S x; s2p (U x) t; s2p S (\<phi> t x) \<longrightarrow> I (\<phi> t x)\<rbrakk> \<Longrightarrow> I (\<phi> t x)
 2. \<And>x t. \<lbrakk>I x; s2p S x; s2p (U x) t; t \<notin> U x\<rbrakk> \<Longrightarrow> I (\<phi> t x)
[PROOF STEP]
using in_domain ivp(2) assms
[PROOF STATE]
proof (prove)
using this:
s2p S ?s \<Longrightarrow> s2p (T \<rightarrow> S) (\<lambda>t. \<phi> t ?s)
s2p S ?s \<Longrightarrow> \<phi> 0 ?s = ?s
s2p S ?s \<Longrightarrow> s2p (U ?s) 0 \<and> is_interval (U ?s) \<and> U ?s \<subseteq> T

goal (2 subgoals):
 1. \<And>x t. \<lbrakk>I x; s2p S x; s2p (U x) t; s2p S (\<phi> t x) \<longrightarrow> I (\<phi> t x)\<rbrakk> \<Longrightarrow> I (\<phi> t x)
 2. \<And>x t. \<lbrakk>I x; s2p S x; s2p (U x) t; t \<notin> U x\<rbrakk> \<Longrightarrow> I (\<phi> t x)
[PROOF STEP]
by force+


[STATEMENT]
lemma diff_inv_eq_inv_set:
  "diff_invariant I (\<lambda>t. f) (\<lambda>s. T) S 0 (\<lambda>s. True) = (\<forall>s. I s \<longrightarrow> \<gamma>\<^sup>\<phi> s \<subseteq> {s. I s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diff_invariant I (\<lambda>t. f) (\<lambda>s. T) S 0 (\<lambda>s. True) = (\<forall>s. I s \<longrightarrow> \<gamma>\<^sup>\<phi> s \<subseteq> {s. I s})
[PROOF STEP]
unfolding diff_inv_eq_inv_set orbit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s. I s \<longrightarrow> x\<acute>=\<lambda>t. f & \<lambda>s. True on \<lambda>s. T S @ 0 s \<subseteq> Collect I) = (\<forall>s. I s \<longrightarrow> x\<acute>=\<lambda>t. f & \<lambda>s. True on \<lambda>s. T S @ 0 s \<subseteq> {s. I s})
[PROOF STEP]
by simp


[STATEMENT]
lemma ffb_g_odei: "P \<le> {s. I s} \<Longrightarrow> {s. I s} \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. I s} \<Longrightarrow>
  {s. I s \<and> G s} \<le> Q \<Longrightarrow> P \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0 DINV I) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq> {s. I s}; {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}; {s. I s \<and> G s} \<subseteq> Q\<rbrakk> \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 DINV I  Q
[PROOF STEP]
unfolding g_ode_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq> {s. I s}; {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}; {s. I s \<and> G s} \<subseteq> Q\<rbrakk> \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
apply(rule_tac b="fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. I s}" in order.trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P \<subseteq> {s. I s}; {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}; {s. I s \<and> G s} \<subseteq> Q\<rbrakk> \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}
 2. \<lbrakk>P \<subseteq> {s. I s}; {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s}; {s. I s \<and> G s} \<subseteq> Q\<rbrakk> \<Longrightarrow> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
apply(rule_tac I="{s. I s}" in ffb_g_orbital_inv, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq> {s. I s}; diff_invariant I f U S t\<^sub>0 G; {s. I s \<and> G s} \<subseteq> Q\<rbrakk> \<Longrightarrow> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
apply(subst ffb_g_orbital_guard, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq> {s. I s}; diff_invariant I f U S t\<^sub>0 G; {s. I s \<and> G s} \<subseteq> Q\<rbrakk> \<Longrightarrow> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. G s \<and> I s} \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
by (rule ffb_iso, force)


[STATEMENT]
lemma diff_solve_axiom1:
  assumes "local_flow f UNIV UNIV \<phi>"
  shows "fb\<^sub>\<F> (x\<acute>= f & G) Q =
  {s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (\<phi> \<tau> s)) \<longrightarrow> (\<phi> t s) \<in> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 Q = {s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s)}
[PROOF STEP]
by (subst local_flow.ffb_g_ode_subset[OF assms], auto)


[STATEMENT]
lemma diff_solve_axiom2:
  fixes c::"'a::{heine_borel, banach}"
  shows "fb\<^sub>\<F> (x\<acute>=(\<lambda>s. c) & G) Q =
  {s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> (s + t *\<^sub>R c) \<in> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=\<lambda>t s. c & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 Q = {s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> s2p Q (s + t *\<^sub>R c)}
[PROOF STEP]
apply(subst local_flow.ffb_g_ode_subset[where \<phi>="(\<lambda>t s. s + t *\<^sub>R c)" and T=UNIV])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. local_flow (\<lambda>s. c) UNIV UNIV (\<lambda>t s. s + t *\<^sub>R c)
 2. \<And>s. s2p UNIV s \<Longrightarrow> s2p (Collect ((\<le>) 0)) 0 \<and> is_interval (Collect ((\<le>) 0)) \<and> Collect ((\<le>) 0) \<subseteq> UNIV
 3. {s. s2p UNIV s \<longrightarrow> (\<forall>t\<in>Collect ((\<le>) 0). (\<forall>\<tau>\<in>down (Collect ((\<le>) 0)) t. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> s2p Q (s + t *\<^sub>R c))} = {s. \<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (s + \<tau> *\<^sub>R c)) \<longrightarrow> s2p Q (s + t *\<^sub>R c)}
[PROOF STEP]
by (rule line_is_local_flow, auto)


[STATEMENT]
lemma diff_solve_rule:
  assumes "local_flow f UNIV UNIV \<phi>"
    and "\<forall>s. s \<in> P \<longrightarrow> (\<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (\<phi> \<tau> s)) \<longrightarrow> (\<phi> t s) \<in> Q)"
  shows "P \<le> fb\<^sub>\<F> (x\<acute>= f & G) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
local_flow f UNIV UNIV \<phi>
\<forall>s. s2p P s \<longrightarrow> (\<forall>t\<ge>0. (\<forall>\<tau>\<in>{0..t}. G (\<phi> \<tau> s)) \<longrightarrow> s2p Q (\<phi> t s))

goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 Q
[PROOF STEP]
by(subst local_flow.ffb_g_ode_subset[OF assms(1)]) auto


[STATEMENT]
lemma diff_weak_axiom1: "s \<in> (fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. G s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2p (fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. G s}) s
[PROOF STEP]
unfolding ffb_eq g_orbital_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2p {s. \<forall>s'. s2p {X t |t X. s2p (U s) t \<and> \<P> X (down (U s) t) \<subseteq> Collect G \<and> s2p (Sols f U S t\<^sub>0 s) X} s' \<longrightarrow> s2p (Collect G) s'} s
[PROOF STEP]
by auto


[STATEMENT]
lemma diff_weak_axiom2: "fb\<^sub>\<F> (x\<acute>= f & G on T S @ t\<^sub>0) Q = fb\<^sub>\<F> (x\<acute>= f & G on T S @ t\<^sub>0) {s. G s \<longrightarrow> s \<in> Q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=f & G on T S @ t\<^sub>0 Q = fb\<^sub>\<F> x\<acute>=f & G on T S @ t\<^sub>0 {s. G s \<longrightarrow> s2p Q s}
[PROOF STEP]
unfolding ffb_g_orbital image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. \<forall>X\<in>Sols f T S t\<^sub>0 s. \<forall>t\<in>T s. (\<forall>\<tau>\<in>down (T s) t. G (X \<tau>)) \<longrightarrow> s2p Q (X t)} = {s. \<forall>X\<in>Sols f T S t\<^sub>0 s. \<forall>t\<in>T s. (\<forall>\<tau>\<in>down (T s) t. G (X \<tau>)) \<longrightarrow> s2p {s. G s \<longrightarrow> s2p Q s} (X t)}
[PROOF STEP]
by force


[STATEMENT]
lemma diff_weak_rule: "{s. G s} \<le> Q \<Longrightarrow> P \<le> fb\<^sub>\<F> (x\<acute>= f & G on T S @ t\<^sub>0) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. G s} \<subseteq> Q \<Longrightarrow> P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on T S @ t\<^sub>0 Q
[PROOF STEP]
by(auto intro: g_orbitalD simp: le_fun_def g_orbital_eq ffb_eq)


[STATEMENT]
lemma ffb_g_orbital_eq_univD:
  assumes "fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. C s} = UNIV"
    and "\<forall>\<tau>\<in>(down (U s) t). x \<tau> \<in> (x\<acute>= f & G on U S @ t\<^sub>0) s"
  shows "\<forall>\<tau>\<in>(down (U s) t). C (x \<tau>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<tau>\<in>down (U s) t. C (x \<tau>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<tau>. s2p (down (U s) t) \<tau> \<Longrightarrow> C (x \<tau>)
[PROOF STEP]
fix \<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<tau>. s2p (down (U s) t) \<tau> \<Longrightarrow> C (x \<tau>)
[PROOF STEP]
assume "\<tau> \<in> (down (U s) t)"
[PROOF STATE]
proof (state)
this:
s2p (down (U s) t) \<tau>

goal (1 subgoal):
 1. \<And>\<tau>. s2p (down (U s) t) \<tau> \<Longrightarrow> C (x \<tau>)
[PROOF STEP]
hence "x \<tau> \<in> (x\<acute>= f & G on U S @ t\<^sub>0) s"
[PROOF STATE]
proof (prove)
using this:
s2p (down (U s) t) \<tau>

goal (1 subgoal):
 1. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (x \<tau>)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
s2p (down (U s) t) \<tau>
\<forall>\<tau>\<in>down (U s) t. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (x \<tau>)

goal (1 subgoal):
 1. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (x \<tau>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (x \<tau>)

goal (1 subgoal):
 1. \<And>\<tau>. s2p (down (U s) t) \<tau> \<Longrightarrow> C (x \<tau>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (x \<tau>)

goal (1 subgoal):
 1. \<And>\<tau>. s2p (down (U s) t) \<tau> \<Longrightarrow> C (x \<tau>)
[PROOF STEP]
have "\<forall>y. y \<in> (x\<acute>= f & G on U S @ t\<^sub>0) s \<longrightarrow> C y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) y \<longrightarrow> C y
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. C s} = UNIV

goal (1 subgoal):
 1. \<forall>y. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) y \<longrightarrow> C y
[PROOF STEP]
unfolding ffb_eq
[PROOF STATE]
proof (prove)
using this:
{s. \<forall>s'. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) s' \<longrightarrow> s2p (Collect C) s'} = UNIV

goal (1 subgoal):
 1. \<forall>y. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) y \<longrightarrow> C y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>y. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) y \<longrightarrow> C y

goal (1 subgoal):
 1. \<And>\<tau>. s2p (down (U s) t) \<tau> \<Longrightarrow> C (x \<tau>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (x \<tau>)
\<forall>y. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) y \<longrightarrow> C y
[PROOF STEP]
show "C (x \<tau>)"
[PROOF STATE]
proof (prove)
using this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (x \<tau>)
\<forall>y. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) y \<longrightarrow> C y

goal (1 subgoal):
 1. C (x \<tau>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C (x \<tau>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_cut_axiom:
  assumes "fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. C s} = UNIV"
  shows "fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) Q = fb\<^sub>\<F> (x\<acute>= f & (\<lambda>s. G s \<and> C s) on U S @ t\<^sub>0) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q = fb\<^sub>\<F> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 Q
[PROOF STEP]
proof(rule_tac f="\<lambda> x. fb\<^sub>\<F> x Q" in HOL.arg_cong, rule ext, rule subset_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
assume "s' \<in> (x\<acute>= f & G on U S @ t\<^sub>0) s"
[PROOF STATE]
proof (state)
this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) s'

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) s'
[PROOF STEP]
obtain \<tau>::real and X where x_ivp: "X \<in> Sols f U S t\<^sub>0 s"
      and "X \<tau> = s'" and "\<tau> \<in> (U s)" and guard_x:"\<P> X (down (U s) \<tau>) \<subseteq> {s. G s}"
[PROOF STATE]
proof (prove)
using this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) s'

goal (1 subgoal):
 1. (\<And>X \<tau>. \<lbrakk>s2p (Sols f U S t\<^sub>0 s) X; X \<tau> = s'; s2p (U s) \<tau>; \<P> X (down (U s) \<tau>) \<subseteq> {s. G s}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using g_orbitalD[of s' "f" G _ S t\<^sub>0 s]
[PROOF STATE]
proof (prove)
using this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) s'
\<lbrakk>s2p (x\<acute>=f & G on ?U S @ t\<^sub>0 s) s'; \<And>X t. \<lbrakk>s2p (Sols f ?U S t\<^sub>0 s) X; X t = s'; s2p (?U s) t; \<P> X (down (?U s) t) \<subseteq> {s. G s}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>X \<tau>. \<lbrakk>s2p (Sols f U S t\<^sub>0 s) X; X \<tau> = s'; s2p (U s) \<tau>; \<P> X (down (U s) \<tau>) \<subseteq> {s. G s}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s2p (Sols f U S t\<^sub>0 s) X
X \<tau> = s'
s2p (U s) \<tau>
\<P> X (down (U s) \<tau>) \<subseteq> {s. G s}

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
have "\<forall>t\<in>(down (U s) \<tau>). \<P> X (down (U s) t) \<subseteq> {s. G s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. \<P> X (down (U s) t) \<subseteq> {s. G s}
[PROOF STEP]
using guard_x
[PROOF STATE]
proof (prove)
using this:
\<P> X (down (U s) \<tau>) \<subseteq> {s. G s}

goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. \<P> X (down (U s) t) \<subseteq> {s. G s}
[PROOF STEP]
by (force simp: image_def)
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>down (U s) \<tau>. \<P> X (down (U s) t) \<subseteq> {s. G s}

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>down (U s) \<tau>. \<P> X (down (U s) t) \<subseteq> {s. G s}

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
have "\<forall>t\<in>(down (U s) \<tau>). t \<in> (U s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. s2p (U s) t
[PROOF STEP]
using \<open>\<tau> \<in> (U s)\<close> closed_segment_subset_interval
[PROOF STATE]
proof (prove)
using this:
s2p (U s) \<tau>
\<lbrakk>is_interval ?T; s2p ?T ?a; s2p ?T ?b\<rbrakk> \<Longrightarrow> {?a--?b} \<subseteq> ?T

goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. s2p (U s) t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>down (U s) \<tau>. s2p (U s) t

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>t\<in>down (U s) \<tau>. \<P> X (down (U s) t) \<subseteq> {s. G s}
\<forall>t\<in>down (U s) \<tau>. s2p (U s) t
[PROOF STEP]
have "\<forall>t\<in>(down (U s) \<tau>). X t \<in> (x\<acute>= f & G on U S @ t\<^sub>0) s"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>down (U s) \<tau>. \<P> X (down (U s) t) \<subseteq> {s. G s}
\<forall>t\<in>down (U s) \<tau>. s2p (U s) t

goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X t)
[PROOF STEP]
using g_orbitalI[OF x_ivp]
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>down (U s) \<tau>. \<P> X (down (U s) t) \<subseteq> {s. G s}
\<forall>t\<in>down (U s) \<tau>. s2p (U s) t
\<lbrakk>s2p (U s) ?t; \<P> X (down (U s) ?t) \<subseteq> {s. ?G s}\<rbrakk> \<Longrightarrow> s2p (x\<acute>=f & ?G on U S @ t\<^sub>0 s) (X ?t)

goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X t)
[PROOF STEP]
by (metis (mono_tags, lifting))
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>down (U s) \<tau>. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X t)

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
hence "\<forall>t\<in>(down (U s) \<tau>). C (X t)"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>down (U s) \<tau>. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X t)

goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. C (X t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>down (U s) \<tau>. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X t)
fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. C s} = UNIV

goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. C (X t)
[PROOF STEP]
unfolding ffb_eq
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>down (U s) \<tau>. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X t)
{s. \<forall>s'. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) s' \<longrightarrow> s2p (Collect C) s'} = UNIV

goal (1 subgoal):
 1. \<forall>t\<in>down (U s) \<tau>. C (X t)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>t\<in>down (U s) \<tau>. C (X t)

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
hence "s' \<in> (x\<acute>= f & (\<lambda>s. G s \<and> C s) on U S @ t\<^sub>0) s"
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>down (U s) \<tau>. C (X t)

goal (1 subgoal):
 1. s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) s'
[PROOF STEP]
using g_orbitalI[OF x_ivp \<open>\<tau> \<in> (U s)\<close>] guard_x \<open>X \<tau> = s'\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>down (U s) \<tau>. C (X t)
\<P> X (down (U s) \<tau>) \<subseteq> {s. ?G s} \<Longrightarrow> s2p (x\<acute>=f & ?G on U S @ t\<^sub>0 s) (X \<tau>)
\<P> X (down (U s) \<tau>) \<subseteq> {s. G s}
X \<tau> = s'

goal (1 subgoal):
 1. s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) s'
[PROOF STEP]
unfolding image_le_pred
[PROOF STATE]
proof (prove)
using this:
\<forall>t\<in>down (U s) \<tau>. C (X t)
\<forall>x\<in>down (U s) \<tau>. ?G (X x) \<Longrightarrow> s2p (x\<acute>=f & ?G on U S @ t\<^sub>0 s) (X \<tau>)
\<forall>x\<in>down (U s) \<tau>. G (X x)
X \<tau> = s'

goal (1 subgoal):
 1. s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) s'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) s'

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) ?s'2 \<Longrightarrow> s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) ?s'2

goal (2 subgoals):
 1. \<And>x. x\<acute>=f & G on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x
 2. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
thus "(x\<acute>= f & G on U S @ t\<^sub>0) s \<subseteq> (x\<acute>= f & (\<lambda>s. G s \<and> C s) on U S @ t\<^sub>0) s"
[PROOF STATE]
proof (prove)
using this:
s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) ?s'2 \<Longrightarrow> s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) ?s'2

goal (1 subgoal):
 1. x\<acute>=f & G on U S @ t\<^sub>0 s \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x\<acute>=f & G on U S @ t\<^sub>0 s \<subseteq> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s

goal (1 subgoal):
 1. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 x \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 x
[PROOF STEP]
show "\<And>s. (x\<acute>= f & (\<lambda>s. G s \<and> C s) on U S @ t\<^sub>0) s \<subseteq> (x\<acute>= f & G on U S @ t\<^sub>0) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 s
[PROOF STEP]
by (auto simp: g_orbital_eq)
[PROOF STATE]
proof (state)
this:
x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 ?s \<subseteq> x\<acute>=f & G on U S @ t\<^sub>0 ?s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_cut_rule:
  assumes ffb_C: "P \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) {s. C s}"
    and ffb_Q: "P \<le> fb\<^sub>\<F> (x\<acute>= f & (\<lambda>s. G s \<and> C s) on U S @ t\<^sub>0) Q"
  shows "P \<le> fb\<^sub>\<F> (x\<acute>= f & G on U S @ t\<^sub>0) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 Q
[PROOF STEP]
proof(subst ffb_eq, subst g_orbital_eq, clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x t X. \<lbrakk>s2p P x; s2p (U x) t; \<forall>xa. s2p (U x) xa \<and> xa \<le> t \<longrightarrow> G (X xa); s2p (Sols f U S t\<^sub>0 x) X\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
fix t::real and X::"real \<Rightarrow> 'a" and s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x t X. \<lbrakk>s2p P x; s2p (U x) t; \<forall>xa. s2p (U x) xa \<and> xa \<le> t \<longrightarrow> G (X xa); s2p (Sols f U S t\<^sub>0 x) X\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
assume "s \<in> P" and "t \<in> (U s)"
    and x_ivp:"X \<in> Sols f U S t\<^sub>0 s"
    and guard_x:"\<forall>\<tau>. \<tau> \<in> (U s) \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)"
[PROOF STATE]
proof (state)
this:
s2p P s
s2p (U s) t
s2p (Sols f U S t\<^sub>0 s) X
\<forall>\<tau>. s2p (U s) \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)

goal (1 subgoal):
 1. \<And>x t X. \<lbrakk>s2p P x; s2p (U x) t; \<forall>xa. s2p (U x) xa \<and> xa \<le> t \<longrightarrow> G (X xa); s2p (Sols f U S t\<^sub>0 x) X\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
have "\<forall>\<tau>\<in>(down (U s) t). X \<tau> \<in> (x\<acute>= f & G on U S @ t\<^sub>0) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<tau>\<in>down (U s) t. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X \<tau>)
[PROOF STEP]
using g_orbitalI[OF x_ivp] guard_x
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s2p (U s) ?t; \<P> X (down (U s) ?t) \<subseteq> {s. ?G s}\<rbrakk> \<Longrightarrow> s2p (x\<acute>=f & ?G on U S @ t\<^sub>0 s) (X ?t)
\<forall>\<tau>. s2p (U s) \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)

goal (1 subgoal):
 1. \<forall>\<tau>\<in>down (U s) t. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X \<tau>)
[PROOF STEP]
unfolding image_le_pred
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s2p (U s) ?t; \<forall>x\<in>down (U s) ?t. ?G (X x)\<rbrakk> \<Longrightarrow> s2p (x\<acute>=f & ?G on U S @ t\<^sub>0 s) (X ?t)
\<forall>\<tau>. s2p (U s) \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)

goal (1 subgoal):
 1. \<forall>\<tau>\<in>down (U s) t. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X \<tau>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<tau>\<in>down (U s) t. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X \<tau>)

goal (1 subgoal):
 1. \<And>x t X. \<lbrakk>s2p P x; s2p (U x) t; \<forall>xa. s2p (U x) xa \<and> xa \<le> t \<longrightarrow> G (X xa); s2p (Sols f U S t\<^sub>0 x) X\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
hence "\<forall>\<tau>\<in>(down (U s) t). C (X \<tau>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<tau>\<in>down (U s) t. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X \<tau>)

goal (1 subgoal):
 1. \<forall>\<tau>\<in>down (U s) t. C (X \<tau>)
[PROOF STEP]
using ffb_C \<open>s \<in> P\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<tau>\<in>down (U s) t. s2p (x\<acute>=f & G on U S @ t\<^sub>0 s) (X \<tau>)
P \<subseteq> fb\<^sub>\<F> x\<acute>=f & G on U S @ t\<^sub>0 {s. C s}
s2p P s

goal (1 subgoal):
 1. \<forall>\<tau>\<in>down (U s) t. C (X \<tau>)
[PROOF STEP]
by (subst (asm) ffb_eq, auto)
[PROOF STATE]
proof (state)
this:
\<forall>\<tau>\<in>down (U s) t. C (X \<tau>)

goal (1 subgoal):
 1. \<And>x t X. \<lbrakk>s2p P x; s2p (U x) t; \<forall>xa. s2p (U x) xa \<and> xa \<le> t \<longrightarrow> G (X xa); s2p (Sols f U S t\<^sub>0 x) X\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
hence "X t \<in> (x\<acute>= f & (\<lambda>s. G s \<and> C s) on U S @ t\<^sub>0) s"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<tau>\<in>down (U s) t. C (X \<tau>)

goal (1 subgoal):
 1. s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) (X t)
[PROOF STEP]
using guard_x \<open>t \<in> (U s)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<tau>\<in>down (U s) t. C (X \<tau>)
\<forall>\<tau>. s2p (U s) \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)
s2p (U s) t

goal (1 subgoal):
 1. s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) (X t)
[PROOF STEP]
by (auto intro!: g_orbitalI x_ivp)
[PROOF STATE]
proof (state)
this:
s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) (X t)

goal (1 subgoal):
 1. \<And>x t X. \<lbrakk>s2p P x; s2p (U x) t; \<forall>xa. s2p (U x) xa \<and> xa \<le> t \<longrightarrow> G (X xa); s2p (Sols f U S t\<^sub>0 x) X\<rbrakk> \<Longrightarrow> s2p Q (X t)
[PROOF STEP]
thus "(X t) \<in> Q"
[PROOF STATE]
proof (prove)
using this:
s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) (X t)

goal (1 subgoal):
 1. s2p Q (X t)
[PROOF STEP]
using \<open>s \<in> P\<close> ffb_Q
[PROOF STATE]
proof (prove)
using this:
s2p (x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 s) (X t)
s2p P s
P \<subseteq> fb\<^sub>\<F> x\<acute>=f & \<lambda>s. G s \<and> C s on U S @ t\<^sub>0 Q

goal (1 subgoal):
 1. s2p Q (X t)
[PROOF STEP]
by (subst (asm) ffb_eq) auto
[PROOF STATE]
proof (state)
this:
s2p Q (X t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_inv_axiom1:
  assumes "G s \<longrightarrow> I s" and "diff_invariant I (\<lambda>t. f) (\<lambda>s. {t. t \<ge> 0}) UNIV 0 G"
  shows "s \<in> (fb\<^sub>\<F> (x\<acute>= f & G) {s. I s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2p (fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 {s. I s}) s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
G s \<longrightarrow> I s
diff_invariant I (\<lambda>t. f) (\<lambda>s. {t. 0 \<le> t}) UNIV 0 G

goal (1 subgoal):
 1. s2p (fb\<^sub>\<F> x\<acute>=\<lambda>t. f & G on \<lambda>s. {t. 0 \<le> t} UNIV @ 0 {s. I s}) s
[PROOF STEP]
unfolding ffb_g_orbital diff_invariant_eq
[PROOF STATE]
proof (prove)
using this:
G s \<longrightarrow> I s
\<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s. \<forall>t\<in>Collect ((\<le>) 0). (\<forall>\<tau>\<in>down (Collect ((\<le>) 0)) t. G (X \<tau>)) \<longrightarrow> I (X t))

goal (1 subgoal):
 1. s2p {s. \<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s. \<forall>t\<in>Collect ((\<le>) 0). (\<forall>\<tau>\<in>down (Collect ((\<le>) 0)) t. G (X \<tau>)) \<longrightarrow> s2p (Collect I) (X t)} s
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>X t. \<lbrakk>G s \<longrightarrow> I s; \<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s. \<forall>t\<ge>0. (\<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)) \<longrightarrow> I (X t)); s2p (Sols (\<lambda>t. f) (\<lambda>s. Collect ((\<le>) 0)) UNIV 0 s) X; 0 \<le> t; \<forall>\<tau>. 0 \<le> \<tau> \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)\<rbrakk> \<Longrightarrow> I (X t)
[PROOF STEP]
by (erule_tac x=s in allE, frule ivp_solsD(2), clarsimp)