# HG changeset patch
# User traytel
# Date 1392801662 -3600
# Node ID 32774e40afb0f8e88a6cf0c4611833b2d9c0f4e1
# Parent  a6c2379078c84e823477e795aa66fadca6c6e1ff
removed not anymore used constants and theorems

diff -r a6c2379078c8 -r 32774e40afb0 src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Wed Feb 19 09:50:50 2014 +0100
+++ b/src/HOL/BNF_GFP.thy	Wed Feb 19 10:21:02 2014 +0100
@@ -10,7 +10,7 @@
 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_GFP
-imports BNF_FP_Base List_Prefix String
+imports BNF_FP_Base String
 keywords
   "codatatype" :: thy_decl and
   "primcorecursive" :: thy_goal and
@@ -149,19 +149,6 @@
 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"
 unfolding convol_def by auto
 
-(*Extended Sublist*)
-
-definition clists where "clists r = |lists (Field r)|"
-
-definition prefCl where
-  "prefCl Kl = (\<forall> kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
-definition PrefCl where
-  "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> prefixeq kl' kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
-
-lemma prefCl_UN:
-  "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
-unfolding prefCl_def PrefCl_def by fastforce
-
 definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
 definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
@@ -169,21 +156,6 @@
 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
 unfolding Shift_def Succ_def by simp
 
-lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
-unfolding Shift_def clists_def Field_card_of by auto
-
-lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
-unfolding prefCl_def Shift_def
-proof safe
-  fix kl1 kl2
-  assume "\<forall>kl1 kl2. prefixeq kl1 kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
-    "prefixeq kl1 kl2" "k # kl2 \<in> Kl"
-  thus "k # kl1 \<in> Kl" using Cons_prefixeq_Cons[of k kl1 k kl2] by blast
-qed
-
-lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
-unfolding Shift_def by simp
-
 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
 unfolding Succ_def by simp
 
@@ -198,13 +170,6 @@
 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
 unfolding Succ_def Shift_def by auto
 
-lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
-unfolding clists_def Field_card_of by auto
-
-lemma Cons_clists:
-  "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
-unfolding clists_def Field_card_of by auto
-
 lemma length_Cons: "length (x # xs) = Suc (length xs)"
 by simp
 
@@ -230,9 +195,6 @@
   toCard A r x = toCard A r y \<longleftrightarrow> x = y"
 using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
 
-lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
-using toCard_pred_toCard unfolding toCard_pred_def by blast
-
 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
 
 lemma fromCard_toCard:
diff -r a6c2379078c8 -r 32774e40afb0 src/HOL/Tools/BNF/bnf_gfp_util.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_util.ML	Wed Feb 19 09:50:50 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_util.ML	Wed Feb 19 10:21:02 2014 +0100
@@ -17,13 +17,10 @@
   val mk_Times: term * term -> term
   val mk_append: term * term -> term
   val mk_congruent: term -> term -> term
-  val mk_clists: term -> term
   val mk_Id_on: term -> term
   val mk_in_rel: term -> term
   val mk_equiv: term -> term -> term
   val mk_fromCard: term -> term -> term
-  val mk_prefCl: term -> term
-  val mk_prefixeq: term -> term -> term
   val mk_proj: term -> term
   val mk_quotient: term -> term -> term
   val mk_rec_list: term -> term -> term
@@ -95,16 +92,6 @@
     Const (@{const_name shift}, T --> dest_listT (Term.domain_type T) --> T) $ lab $ k
   end;
 
-fun mk_prefCl A =
-  Const (@{const_name prefCl}, fastype_of A --> HOLogic.boolT) $ A;
-
-fun mk_prefixeq xs ys =
-  Const (@{const_name prefixeq}, fastype_of xs --> fastype_of ys --> HOLogic.boolT) $ xs $ ys;
-
-fun mk_clists r =
-  let val T = fastype_of r;
-  in Const (@{const_name clists}, T --> mk_relT (`I (HOLogic.listT (fst (dest_relT T))))) $ r end;
-
 fun mk_toCard A r =
   let
     val AT = fastype_of A;