src/HOL/BNF/BNF_GFP.thy
changeset 52660 7f7311d04727
parent 52659 58b87aa4dc3b
child 52731 dacd47a0633f
     1.1 --- a/src/HOL/BNF/BNF_GFP.thy	Mon Jul 15 14:23:51 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Mon Jul 15 15:50:39 2013 +0200
     1.3 @@ -174,9 +174,6 @@
     1.4  lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
     1.5  by simp
     1.6  
     1.7 -lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}"
     1.8 -by auto
     1.9 -
    1.10  lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x"
    1.11  unfolding convol_def by auto
    1.12  
    1.13 @@ -213,14 +210,6 @@
    1.14  lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
    1.15  unfolding Shift_def by simp
    1.16  
    1.17 -lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
    1.18 -unfolding Succ_def proof
    1.19 -  assume "prefCl Kl" "k # kl \<in> Kl"
    1.20 -  moreover have "prefixeq (k # []) (k # kl)" by auto
    1.21 -  ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
    1.22 -  thus "[] @ [k] \<in> Kl" by simp
    1.23 -qed
    1.24 -
    1.25  lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
    1.26  unfolding Succ_def by simp
    1.27  
    1.28 @@ -235,18 +224,6 @@
    1.29  lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
    1.30  unfolding Succ_def Shift_def by auto
    1.31  
    1.32 -lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k"
    1.33 -unfolding Shift_def by simp
    1.34 -
    1.35 -lemma Func_cexp: "|Func A B| =o |B| ^c |A|"
    1.36 -unfolding cexp_def Field_card_of by (simp only: card_of_refl)
    1.37 -
    1.38 -lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r"
    1.39 -unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
    1.40 -
    1.41 -lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
    1.42 -unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto
    1.43 -
    1.44  lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
    1.45  unfolding clists_def Field_card_of by auto
    1.46