tuned proofs
authorhaftmann
Sat Dec 24 15:53:09 2011 +0100 (2011-12-24)
changeset 4596603ce2b2a29a2
parent 45965 2af982715e5c
child 45967 76cf71ed15c7
tuned proofs
src/HOL/Library/Reflection.thy
src/HOL/Nominal/Examples/Standardization.thy
src/HOL/RComplete.thy
src/HOL/SupInf.thy
src/HOL/ex/Set_Theory.thy
     1.1 --- a/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
     1.2 +++ b/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  setup {* Reify_Data.setup *}
     1.5  
     1.6  lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
     1.7 -  by (blast intro: ext)
     1.8 +  by blast
     1.9  
    1.10  use "reflection.ML"
    1.11  
     2.1 --- a/src/HOL/Nominal/Examples/Standardization.thy	Sat Dec 24 15:53:09 2011 +0100
     2.2 +++ b/src/HOL/Nominal/Examples/Standardization.thy	Sat Dec 24 15:53:09 2011 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Standardization *}
     2.5  
     2.6  theory Standardization
     2.7 -imports Nominal
     2.8 +imports "../Nominal"
     2.9  begin
    2.10  
    2.11  text {*
    2.12 @@ -426,11 +426,7 @@
    2.13  lemma listrelp_eqvt [eqvt]:
    2.14    assumes xy: "listrelp f (x::'a::pt_name list) y"
    2.15    shows "listrelp ((pi::name prm) \<bullet> f) (pi \<bullet> x) (pi \<bullet> y)" using xy
    2.16 -  apply induct
    2.17 -   apply (simp add: listrelp.intros)
    2.18 -  apply simp
    2.19 -  apply (metis listrelp.Cons in_eqvt mem_def perm_app pt_set_bij3)
    2.20 -  done
    2.21 +  by induct (simp_all add: listrelp.intros perm_app [symmetric])
    2.22  
    2.23  inductive
    2.24    sred :: "lam \<Rightarrow> lam \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>s" 50)
     3.1 --- a/src/HOL/RComplete.thy	Sat Dec 24 15:53:09 2011 +0100
     3.2 +++ b/src/HOL/RComplete.thy	Sat Dec 24 15:53:09 2011 +0100
     3.3 @@ -76,8 +76,7 @@
     3.4    from assms have "\<exists>X. X \<in> S" and "\<exists>Y. \<forall>x\<in>S. x \<le> Y"
     3.5      unfolding isUb_def setle_def by simp_all
     3.6    from complete_real [OF this] show ?thesis
     3.7 -    unfolding isLub_def leastP_def setle_def setge_def Ball_def
     3.8 -      Collect_def mem_def isUb_def UNIV_def by simp
     3.9 +    by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
    3.10  qed
    3.11  
    3.12  
     4.1 --- a/src/HOL/SupInf.thy	Sat Dec 24 15:53:09 2011 +0100
     4.2 +++ b/src/HOL/SupInf.thy	Sat Dec 24 15:53:09 2011 +0100
     4.3 @@ -356,7 +356,7 @@
     4.4  lemma Inf_greater:
     4.5    fixes z :: real
     4.6    shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
     4.7 -  by (metis Inf_real_iff mem_def not_leE)
     4.8 +  by (metis Inf_real_iff not_leE)
     4.9  
    4.10  lemma Inf_close:
    4.11    fixes e :: real
     5.1 --- a/src/HOL/ex/Set_Theory.thy	Sat Dec 24 15:53:09 2011 +0100
     5.2 +++ b/src/HOL/ex/Set_Theory.thy	Sat Dec 24 15:53:09 2011 +0100
     5.3 @@ -179,7 +179,7 @@
     5.4  
     5.5  lemma "a < b \<and> b < (c::int) \<Longrightarrow> \<exists>A. a \<notin> A \<and> b \<in> A \<and> c \<notin> A"
     5.6    -- {* Example 4. *}
     5.7 -  by force
     5.8 +  by auto --{*slow*}
     5.9  
    5.10  lemma "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
    5.11    -- {*Example 5, page 298. *}
    5.12 @@ -194,9 +194,9 @@
    5.13    by force
    5.14  
    5.15  lemma "(\<forall>u v. u < (0::int) \<longrightarrow> u \<noteq> abs v)
    5.16 -    \<longrightarrow> (\<exists>A::int set. (\<forall>y. abs y \<notin> A) \<and> -2 \<in> A)"
    5.17 -  -- {* Example 8 now needs a small hint. *}
    5.18 -  by (simp add: abs_if, force)
    5.19 +    \<longrightarrow> (\<exists>A::int set. -2 \<in> A & (\<forall>y. abs y \<notin> A))"
    5.20 +  -- {* Example 8 needs a small hint. *}
    5.21 +  by force
    5.22      -- {* not @{text blast}, which can't simplify @{text "-2 < 0"} *}
    5.23  
    5.24  text {* Example 9 omitted (requires the reals). *}