less flex-flex pairs
authornoschinl
Thu Feb 20 15:14:37 2014 +0100 (2014-02-20)
changeset 5560442e4e8c2e8dc
parent 55603 48596c45bf7f
child 55605 b1b363e81c87
child 55606 75a639ddc05f
less flex-flex pairs
src/HOL/BNF_Cardinal_Arithmetic.thy
src/HOL/Inductive.thy
src/HOL/Lifting.thy
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Thu Feb 20 13:53:26 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Thu Feb 20 15:14:37 2014 +0100
     1.3 @@ -400,7 +400,8 @@
     1.4    proof (cases "Field p2 = {}")
     1.5      case True
     1.6      with n have "Field r2 = {}" .
     1.7 -    hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI)
     1.8 +    hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def
     1.9 +      by (auto intro: card_of_ordLeqI[where f="\<lambda>_ _. undefined"])
    1.10      thus ?thesis using `p1 ^c p2 \<le>o cone` ordLeq_transitive by auto
    1.11    next
    1.12      case False with True have "|Field (p1 ^c p2)| =o czero"
     2.1 --- a/src/HOL/Inductive.thy	Thu Feb 20 13:53:26 2014 +0100
     2.2 +++ b/src/HOL/Inductive.thy	Thu Feb 20 15:14:37 2014 +0100
     2.3 @@ -177,12 +177,13 @@
     2.4  
     2.5  text{*strong version, thanks to Coen and Frost*}
     2.6  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
     2.7 -  by (blast intro: weak_coinduct [OF _ coinduct_lemma])
     2.8 +  by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
     2.9  
    2.10  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
    2.11    apply (rule order_trans)
    2.12    apply (rule sup_ge1)
    2.13 -  apply (erule gfp_upperbound [OF coinduct_lemma])
    2.14 +  apply (rule gfp_upperbound)
    2.15 +  apply (erule coinduct_lemma)
    2.16    apply assumption
    2.17    done
    2.18  
     3.1 --- a/src/HOL/Lifting.thy	Thu Feb 20 13:53:26 2014 +0100
     3.2 +++ b/src/HOL/Lifting.thy	Thu Feb 20 15:14:37 2014 +0100
     3.3 @@ -455,13 +455,13 @@
     3.4    assumes "left_unique T"
     3.5    assumes "R \<le> op="
     3.6    shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
     3.7 -using assms unfolding left_unique_def by fast
     3.8 +using assms unfolding left_unique_def by blast
     3.9  
    3.10  lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
    3.11  unfolding left_total_def OO_def by fast
    3.12  
    3.13  lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
    3.14 -unfolding left_unique_def OO_def by fast
    3.15 +unfolding left_unique_def OO_def by blast
    3.16  
    3.17  lemma invariant_le_eq:
    3.18    "invariant P \<le> op=" unfolding invariant_def by blast