src/HOL/BNF_Least_Fixpoint.thy
changeset 58136 10f92532f128
parent 58128 43a1ba26a8cb
child 58147 967444d352b8
equal deleted inserted replaced
58134:b563ec62d04e 58136:10f92532f128
   153 qed
   153 qed
   154 
   154 
   155 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
   155 lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
   156 by auto
   156 by auto
   157 
   157 
   158 (*helps resolution*)
   158 lemmas well_order_induct_imp = wo_rel.well_order_induct[of r "\<lambda>x. x \<in> Field r \<longrightarrow> P x" for r P]
   159 lemma well_order_induct_imp:
       
   160   "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>
       
   161      x \<in> Field r \<longrightarrow> P x"
       
   162 by (erule wo_rel.well_order_induct)
       
   163 
   159 
   164 lemma meta_spec2:
   160 lemma meta_spec2:
   165   assumes "(\<And>x y. PROP P x y)"
   161   assumes "(\<And>x y. PROP P x y)"
   166   shows "PROP P x y"
   162   shows "PROP P x y"
   167 by (rule assms)
   163   by (rule assms)
   168 
   164 
   169 lemma nchotomy_relcomppE:
   165 lemma nchotomy_relcomppE:
   170   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"
   166   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"
   171   shows P
   167   shows P
   172 proof (rule relcompp.cases[OF assms(2)], hypsubst)
   168 proof (rule relcompp.cases[OF assms(2)], hypsubst)