src/HOL/BNF_Least_Fixpoint.thy
changeset 58136 10f92532f128
parent 58128 43a1ba26a8cb
child 58147 967444d352b8
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 02 08:24:42 2014 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 02 12:09:13 2014 +0200
     1.3 @@ -155,16 +155,12 @@
     1.4  lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
     1.5  by auto
     1.6  
     1.7 -(*helps resolution*)
     1.8 -lemma well_order_induct_imp:
     1.9 -  "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
    1.10 -     x \<in> Field r \<longrightarrow> P x"
    1.11 -by (erule wo_rel.well_order_induct)
    1.12 +lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\<lambda>x. x \<in> Field r \<longrightarrow> P x" for r P]
    1.13  
    1.14  lemma meta_spec2:
    1.15    assumes "(\<And>x y. PROP P x y)"
    1.16    shows "PROP P x y"
    1.17 -by (rule assms)
    1.18 +  by (rule assms)
    1.19  
    1.20  lemma nchotomy_relcomppE:
    1.21    assumes "\<And>y. \<exists>x. y = f x" "(r OO s) a c" "\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P"