--- 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:
--- 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;