[STATEMENT]
lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x\<bar> \<le> 1 \<Longrightarrow> complex_of_real (arcsin x) = Arcsin (complex_of_real x)
[PROOF STEP]
by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)


[STATEMENT]
lemma ceiling_le_numeral [simp]: "\<lceil>x\<rceil> \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lceil>x\<rceil> \<le> numeral v) = (x \<le> numeral v)
[PROOF STEP]
by (simp add: ceiling_le_iff)


[STATEMENT]
lemma U_F2: "Mutex \<in> {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mutex \<in> {s. \<not> p s \<and> m s = 2} \<longmapsto>w {s. m s = 3}
[PROOF STEP]
apply (cut_tac IU)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mutex \<in> Always IU \<Longrightarrow> Mutex \<in> {s. \<not> p s \<and> m s = 2} \<longmapsto>w {s. m s = 3}
[PROOF STEP]
apply (unfold Mutex_def, ensures_tac U2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tan_mono_le: "-(pi/2) < x \<Longrightarrow> x \<le> y \<Longrightarrow> y < pi/2 \<Longrightarrow> tan x \<le> tan y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- (pi / 2) < x; x \<le> y; y < pi / 2\<rbrakk> \<Longrightarrow> tan x \<le> tan y
[PROOF STEP]
using less_eq_real_def tan_monotone
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
\<lbrakk>- (pi / 2) < ?y; ?y < ?x; ?x < pi / 2\<rbrakk> \<Longrightarrow> tan ?y < tan ?x

goal (1 subgoal):
 1. \<lbrakk>- (pi / 2) < x; x \<le> y; y < pi / 2\<rbrakk> \<Longrightarrow> tan x \<le> tan y
[PROOF STEP]
by auto


[STATEMENT]
lemma arctan_minus: "arctan (- x) = - arctan x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arctan (- x) = - arctan x
[PROOF STEP]
using arctan [of "x"]
[PROOF STATE]
proof (prove)
using this:
- (pi / 2) < arctan x \<and> arctan x < pi / 2 \<and> tan (arctan x) = x

goal (1 subgoal):
 1. arctan (- x) = - arctan x
[PROOF STEP]
by (auto simp: arctan_unique)


[STATEMENT]
lemma tanh_real_at_top: "(tanh \<longlongrightarrow> (1::real)) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
have "((\<lambda>x::real. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top
[PROOF STEP]
by (intro tendsto_intros filterlim_compose[OF exp_at_bot]
              filterlim_tendsto_neg_mult_at_bot[OF tendsto_const] filterlim_ident) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top

goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top

goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
have "(\<lambda>x::real. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) = tanh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) = tanh
[PROOF STEP]
by (rule ext) (simp add: tanh_real_altdef)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) = tanh

goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(tanh \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(tanh \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top

goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(tanh \<longlongrightarrow> 1) at_top

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "sqrt 196 = 14"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt 196 = 14
[PROOF STEP]
by simp


[STATEMENT]
lemma card_of_Un_ordLeq_infinite[simp]:
assumes C: "\<not>finite C" and A: "|A| \<le>o |C|" and B: "|B| \<le>o |C|"
shows "|A Un B| \<le>o |C|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |A \<union> B| \<le>o |C|
[PROOF STEP]
using assms card_of_Plus_ordLeq_infinite card_of_Un_Plus_ordLeq
ordLeq_transitive
[PROOF STATE]
proof (prove)
using this:
infinite C
|A| \<le>o |C|
|B| \<le>o |C|
\<lbrakk>infinite ?C; |?A| \<le>o |?C|; |?B| \<le>o |?C|\<rbrakk> \<Longrightarrow> |?A <+> ?B| \<le>o |?C|
|?A \<union> ?B| \<le>o |?A <+> ?B|
\<lbrakk>?r \<le>o ?r'; ?r' \<le>o ?r''\<rbrakk> \<Longrightarrow> ?r \<le>o ?r''

goal (1 subgoal):
 1. |A \<union> B| \<le>o |C|
[PROOF STEP]
by metis


[STATEMENT]
lemma lim_nslim_iff: "lim X = nslim X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lim X = nslim X
[PROOF STEP]
by (simp add: lim_def nslim_def LIMSEQ_NSLIMSEQ_iff)


[STATEMENT]
lemma relative_to_subset:
   "S \<subseteq> T \<and> P S \<Longrightarrow> (P relative_to T) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> T \<and> P S \<Longrightarrow> (P relative_to T) S
[PROOF STEP]
unfolding relative_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> T \<and> P S \<Longrightarrow> \<exists>U. P U \<and> T \<inter> U = S
[PROOF STEP]
by auto


[STATEMENT]
lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
  for x :: "'a::{perfect_space,metric_space}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r
[PROOF STEP]
using islimpt_UNIV [of x]
[PROOF STATE]
proof (prove)
using this:
x islimpt UNIV

goal (1 subgoal):
 1. 0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r
[PROOF STEP]
by (simp add: islimpt_approachable)


[STATEMENT]
lemma continuous_onE:
    assumes "continuous_on s f" "x\<in>s" "e>0"
    obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on s f
x \<in> s
0 < e

goal (1 subgoal):
 1. (\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: continuous_on_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis; \<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e; x \<in> s; 0 < e\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (elim ballE allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis; x \<in> s; 0 < e; 0 < ?e6 \<longrightarrow> (\<exists>d>0. \<forall>x'\<in>s. dist x' ?x5 < d \<longrightarrow> dist (f x') (f ?x5) < ?e6)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis; x \<in> s; 0 < e; ?x5 \<notin> s\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto intro: that [where d="d/2" for d])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sum_choose_upper: "(\<Sum>k\<le>n. k choose m) = Suc n choose Suc m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<le>n. k choose m) = Suc n choose Suc m
[PROOF STEP]
by (induct n) auto


[STATEMENT]
lemma univ_preserves:
  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
  shows "\<forall>X \<in> A//r. univ f X \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>X\<in>A // r. univ f X \<in> B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
assume "X \<in> A//r"
[PROOF STATE]
proof (state)
this:
X \<in> A // r

goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<in> A // r
[PROOF STEP]
obtain x where x: "x \<in> A" and X: "X = proj r x"
[PROOF STATE]
proof (prove)
using this:
X \<in> A // r

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; X = proj r x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ECH proj_image[of r A]
[PROOF STATE]
proof (prove)
using this:
X \<in> A // r
equiv A r
proj r ` A = A // r

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> A; X = proj r x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> A
X = proj r x

goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
hence "univ f X = f x"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
X = proj r x

goal (1 subgoal):
 1. univ f X = f x
[PROOF STEP]
using ECH RES univ_commute
[PROOF STATE]
proof (prove)
using this:
x \<in> A
X = proj r x
equiv A r
f respects r
\<lbrakk>equiv ?A ?r; ?f respects ?r; ?x \<in> ?A\<rbrakk> \<Longrightarrow> univ ?f (proj ?r ?x) = ?f ?x

goal (1 subgoal):
 1. univ f X = f x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
univ f X = f x

goal (1 subgoal):
 1. \<And>X. X \<in> A // r \<Longrightarrow> univ f X \<in> B
[PROOF STEP]
thus "univ f X \<in> B"
[PROOF STATE]
proof (prove)
using this:
univ f X = f x

goal (1 subgoal):
 1. univ f X \<in> B
[PROOF STEP]
using x PRES
[PROOF STATE]
proof (prove)
using this:
univ f X = f x
x \<in> A
\<forall>x\<in>A. f x \<in> B

goal (1 subgoal):
 1. univ f X \<in> B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
univ f X \<in> B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem welltyped_aggressive_imp_defensive:
  "wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s \<midarrow>jvm\<rightarrow> t
  \<Longrightarrow> G \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> t\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal t
[PROOF STEP]
apply (unfold exec_all_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; (s, t) \<in> {(s, t). exec (G, s) = Some t}\<^sup>*\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal t
[PROOF STEP]
apply (erule rtrancl_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal s
 2. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; (s, y) \<in> {(s, t). exec (G, s) = Some t}\<^sup>*; (y, z) \<in> {(s, t). exec (G, s) = Some t}; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (simp add: exec_all_d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; (s, y) \<in> {(s, t). exec (G, s) = Some t}\<^sup>*; (y, z) \<in> {(s, t). exec (G, s) = Some t}; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; (s, y) \<in> {(s, t). exec (G, s) = Some t}\<^sup>*; exec (G, y) = Some z; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (fold exec_all_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (frule BV_correct, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>wt_jvm_prog G Phi; G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y; G,Phi \<turnstile>JVM y \<surd>\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal y; G,Phi \<turnstile>JVM y \<surd>; exec_d G (Normal y) = Normal (Some z)\<rbrakk> \<Longrightarrow> G \<turnstile> Normal s \<midarrow>jvmd\<rightarrow> Normal z
[PROOF STEP]
apply (simp add: exec_all_d_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; (Normal s, Normal y) \<in> ({s. exec_d G s = TypeError} \<times> {TypeError} \<union> {(s, t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*; G,Phi \<turnstile>JVM y \<surd>; exec_d G (Normal y) = Normal (Some z)\<rbrakk> \<Longrightarrow> (Normal s, Normal z) \<in> ({s. exec_d G s = TypeError} \<times> {TypeError} \<union> {(s, t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*
[PROOF STEP]
apply (rule rtrancl_trans, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>G,Phi \<turnstile>JVM s \<surd>; G \<turnstile> s \<midarrow>jvm\<rightarrow> y; exec (G, y) = Some z; (Normal s, Normal y) \<in> ({s. exec_d G s = TypeError} \<times> {TypeError} \<union> {(s, t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*; G,Phi \<turnstile>JVM y \<surd>; exec_d G (Normal y) = Normal (Some z)\<rbrakk> \<Longrightarrow> (Normal y, Normal z) \<in> ({s. exec_d G s = TypeError} \<times> {TypeError} \<union> {(s, t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nat_less_real_le: "n < m \<longleftrightarrow> real n + 1 \<le> real m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n < m) = (real n + 1 \<le> real m)
[PROOF STEP]
by (metis discrete of_nat_1 of_nat_add of_nat_le_iff)


[STATEMENT]
lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<le> g s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<in> f Fols g \<Longrightarrow> F \<in> Always {s. f s \<le> g s}
[PROOF STEP]
by (simp add: Follows_def)


[STATEMENT]
lemma real_root_Suc_0 [simp]: "root (Suc 0) x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (Suc 0) x = x
[PROOF STEP]
by (simp add: odd_real_root_unique)