--- a/src/HOL/Codatatype/Examples/HFset.thy Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/HFset.thy Tue Sep 04 17:23:08 2012 +0200
@@ -48,13 +48,13 @@
subsection{* Recursion and iteration *}
-lemma hfset_rec:
-"hfset_rec R (Fold hs) = R (map_fset <id, hfset_rec R> hs)"
-using hfset.rec unfolding Fold_def .
+lemma hfset_fld_rec:
+"hfset_fld_rec R (Fold hs) = R (map_fset <id, hfset_fld_rec R> hs)"
+using hfset.fld_rec unfolding Fold_def .
(* The iterator has a simpler form: *)
-lemma hfset_iter:
-"hfset_iter R (Fold hs) = R (map_fset (hfset_iter R) hs)"
-using hfset.iter unfolding Fold_def .
+lemma hfset_fld_iter:
+"hfset_fld_iter R (Fold hs) = R (map_fset (hfset_fld_iter R) hs)"
+using hfset.fld_iter unfolding Fold_def .
end
--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Tue Sep 04 17:23:08 2012 +0200
@@ -24,20 +24,20 @@
(* These should be eventually inferred from compositionality *)
-lemma TreeBNF_map:
-"TreeBNF_map f (n,as) = (n, map_fset (id \<oplus> f) as)"
-unfolding TreeBNF_map_def id_apply
-sum_map_def by simp
+lemma TreeBNF_map:
+"TreeBNF_map f (n, as) = (n, map_fset (id \<oplus> f) as)"
+unfolding TreeBNF_map_def id_apply
+sum_map_def by simp
lemma TreeBNF_map':
"TreeBNF_map f n_as = (fst n_as, map_fset (id \<oplus> f) (snd n_as))"
using TreeBNF_map by(cases n_as, simp)
-definition
-"llift2 \<phi> as1 as2 \<longleftrightarrow>
- (\<forall> n. Inl n \<in> fset as1 \<longleftrightarrow> Inl n \<in> fset as2) \<and>
- (\<forall> tr1. Inr tr1 \<in> fset as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> fset as2 \<and> \<phi> tr1 tr2)) \<and>
+definition
+"llift2 \<phi> as1 as2 \<longleftrightarrow>
+ (\<forall> n. Inl n \<in> fset as1 \<longleftrightarrow> Inl n \<in> fset as2) \<and>
+ (\<forall> tr1. Inr tr1 \<in> fset as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> fset as2 \<and> \<phi> tr1 tr2)) \<and>
(\<forall> tr2. Inr tr2 \<in> fset as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> fset as1 \<and> \<phi> tr1 tr2))"
lemma TreeBNF_pred: "TreeBNF_pred \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> as1 as2"
@@ -65,7 +65,7 @@
(* These are mere auxiliaries *)
definition "asNNode tr \<equiv> SOME n_as. NNode (fst n_as) (snd n_as) = tr"
-lemmas pre_sel_defs = asNNode_def
+lemmas pre_sel_defs = asNNode_def
subsection {* Selectors *}
@@ -84,9 +84,9 @@
(* Constructors versus selectors *)
lemma NNode_surj: "\<exists> n as. NNode n as = tr"
unfolding NNode_def
-by (metis Tree.fld_unf pair_collapse)
+by (metis Tree.fld_unf pair_collapse)
-lemma NNode_asNNode:
+lemma NNode_asNNode:
"NNode (fst (asNNode tr)) (snd (asNNode tr)) = tr"
proof-
obtain n as where "NNode n as = tr" using NNode_surj[of tr] by blast
@@ -94,12 +94,12 @@
thus ?thesis unfolding asNNode_def by(rule someI)
qed
-theorem NNode_root_ccont[simp]:
+theorem NNode_root_ccont[simp]:
"NNode (root tr) (ccont tr) = tr"
using NNode_asNNode unfolding root_def ccont_def .
(* Constructors *)
-theorem TTree_simps[simp]:
+theorem TTree_simps[simp]:
"NNode n as = NNode n' as' \<longleftrightarrow> n = n' \<and> as = as'"
unfolding ctor_defs Tree.fld_inject by auto
@@ -109,7 +109,7 @@
proof(cases rule: Tree.fld_exhaust[of tr])
fix x assume "tr = Tree_fld x"
thus ?thesis
- apply(cases x)
+ apply(cases x)
using NNode unfolding ctor_defs apply blast
done
qed
@@ -125,33 +125,33 @@
subsection{* Coinduction *}
theorem TTree_coind_Node[elim, consumes 1, case_names NNode, induct pred: "HOL.eq"]:
-assumes phi: "\<phi> tr1 tr2" and
-NNode: "\<And> n1 n2 as1 as2.
- \<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow>
+assumes phi: "\<phi> tr1 tr2" and
+NNode: "\<And> n1 n2 as1 as2.
+ \<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow>
n1 = n2 \<and> llift2 \<phi> as1 as2"
shows "tr1 = tr2"
apply(rule mp[OF Tree.pred_coinduct[of \<phi> tr1 tr2] phi]) proof clarify
fix tr1 tr2 assume \<phi>: "\<phi> tr1 tr2"
- show "TreeBNF_pred \<phi> (Tree_unf tr1) (Tree_unf tr2)"
+ show "TreeBNF_pred \<phi> (Tree_unf tr1) (Tree_unf tr2)"
apply(cases rule: Tree.fld_exhaust[of tr1], cases rule: Tree.fld_exhaust[of tr2])
- apply (simp add: Tree.unf_fld)
+ apply (simp add: Tree.unf_fld)
apply(case_tac x, case_tac xa, simp)
unfolding TreeBNF_pred apply(rule NNode) using \<phi> unfolding NNode_def by simp
qed
theorem TTree_coind[elim, consumes 1, case_names LLift]:
-assumes phi: "\<phi> tr1 tr2" and
-LLift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
+assumes phi: "\<phi> tr1 tr2" and
+LLift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
root tr1 = root tr2 \<and> llift2 \<phi> (ccont tr1) (ccont tr2)"
shows "tr1 = tr2"
using phi apply(induct rule: TTree_coind_Node)
-using LLift by (metis TTree_sel_ctor)
+using LLift by (metis TTree_sel_ctor)
subsection {* Coiteration *}
-
-(* Preliminaries: *)
+
+(* Preliminaries: *)
declare Tree.unf_fld[simp]
declare Tree.fld_unf[simp]
@@ -162,40 +162,40 @@
lemma Tree_unf_root_ccont:
"Tree_unf tr = (root tr, ccont tr)"
unfolding root_def ccont_def
-by (metis (lifting) NNode_asNNode Tree_unf_NNode)
+by (metis (lifting) NNode_asNNode Tree_unf_NNode)
(* Coiteration *)
-definition TTree_coit ::
+definition TTree_coit ::
"('b \<Rightarrow> N) \<Rightarrow> ('b \<Rightarrow> (T + 'b) fset) \<Rightarrow> 'b \<Rightarrow> Tree"
-where "TTree_coit rt ct \<equiv> Tree_coiter <rt,ct>"
+where "TTree_coit rt ct \<equiv> Tree_unf_coiter <rt,ct>"
-lemma Tree_coit_coit:
-"Tree_coiter s = TTree_coit (fst o s) (snd o s)"
+lemma Tree_coit_coit:
+"Tree_unf_coiter s = TTree_coit (fst o s) (snd o s)"
apply(rule ext)
unfolding TTree_coit_def by simp
-theorem TTree_coit:
-"root (TTree_coit rt ct b) = rt b"
+theorem TTree_coit:
+"root (TTree_coit rt ct b) = rt b"
"ccont (TTree_coit rt ct b) = map_fset (id \<oplus> TTree_coit rt ct) (ct b)"
-using Tree.coiter[of "<rt,ct>" b] unfolding Tree_coit_coit fst_convol snd_convol
-unfolding TreeBNF_map' fst_convol' snd_convol'
-unfolding Tree_unf_root_ccont by simp_all
+using Tree.unf_coiter[of "<rt,ct>" b] unfolding Tree_coit_coit fst_convol snd_convol
+unfolding TreeBNF_map' fst_convol' snd_convol'
+unfolding Tree_unf_root_ccont by simp_all
-(* Corecursion, stronger than coitation *)
-definition TTree_corec ::
+(* Corecursion, stronger than coiteration *)
+definition TTree_corec ::
"('b \<Rightarrow> N) \<Rightarrow> ('b \<Rightarrow> (T + (Tree + 'b)) fset) \<Rightarrow> 'b \<Rightarrow> Tree"
-where "TTree_corec rt ct \<equiv> Tree_corec <rt,ct>"
+where "TTree_corec rt ct \<equiv> Tree_unf_corec <rt,ct>"
-lemma Tree_corec_corec:
-"Tree_corec s = TTree_corec (fst o s) (snd o s)"
+lemma Tree_unf_corec_corec:
+"Tree_unf_corec s = TTree_corec (fst o s) (snd o s)"
apply(rule ext)
unfolding TTree_corec_def by simp
-theorem TTree_corec:
-"root (TTree_corec rt ct b) = rt b"
+theorem TTree_corec:
+"root (TTree_corec rt ct b) = rt b"
"ccont (TTree_corec rt ct b) = map_fset (id \<oplus> ([[id, TTree_corec rt ct]]) ) (ct b)"
-using Tree.corec[of "<rt,ct>" b] unfolding Tree_corec_corec fst_convol snd_convol
-unfolding TreeBNF_map' fst_convol' snd_convol'
+using Tree.unf_corec[of "<rt,ct>" b] unfolding Tree_unf_corec_corec fst_convol snd_convol
+unfolding TreeBNF_map' fst_convol' snd_convol'
unfolding Tree_unf_root_ccont by simp_all
@@ -206,39 +206,39 @@
definition "coit rt ct \<equiv> TTree_coit rt (the_inv fset o ct)"
definition "corec rt ct \<equiv> TTree_corec rt (the_inv fset o ct)"
-definition lift ("_ ^#" 200) where
+definition lift ("_ ^#" 200) where
"lift \<phi> as \<longleftrightarrow> (\<forall> tr. Inr tr \<in> as \<longrightarrow> \<phi> tr)"
-definition lift2 ("_ ^#2" 200) where
-"lift2 \<phi> as1 as2 \<longleftrightarrow>
- (\<forall> n. Inl n \<in> as1 \<longleftrightarrow> Inl n \<in> as2) \<and>
- (\<forall> tr1. Inr tr1 \<in> as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> as2 \<and> \<phi> tr1 tr2)) \<and>
+definition lift2 ("_ ^#2" 200) where
+"lift2 \<phi> as1 as2 \<longleftrightarrow>
+ (\<forall> n. Inl n \<in> as1 \<longleftrightarrow> Inl n \<in> as2) \<and>
+ (\<forall> tr1. Inr tr1 \<in> as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> as2 \<and> \<phi> tr1 tr2)) \<and>
(\<forall> tr2. Inr tr2 \<in> as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> as1 \<and> \<phi> tr1 tr2))"
-definition liftS ("_ ^#s" 200) where
+definition liftS ("_ ^#s" 200) where
"liftS trs = {as. Inr -` as \<subseteq> trs}"
-lemma lift2_llift2:
-"\<lbrakk>finite as1; finite as2\<rbrakk> \<Longrightarrow>
+lemma lift2_llift2:
+"\<lbrakk>finite as1; finite as2\<rbrakk> \<Longrightarrow>
lift2 \<phi> as1 as2 \<longleftrightarrow> llift2 \<phi> (the_inv fset as1) (the_inv fset as2)"
unfolding lift2_def llift2_def by auto
-lemma llift2_lift2:
+lemma llift2_lift2:
"llift2 \<phi> as1 as2 \<longleftrightarrow> lift2 \<phi> (fset as1) (fset as2)"
using lift2_llift2 by (metis finite_fset fset_cong fset_to_fset)
lemma mono_lift:
-assumes "(\<phi>^#) as"
+assumes "(\<phi>^#) as"
and "\<And> tr. \<phi> tr \<Longrightarrow> \<phi>' tr"
shows "(\<phi>'^#) as"
using assms unfolding lift_def[abs_def] by blast
lemma mono_liftS:
assumes "trs1 \<subseteq> trs2 "
-shows "(trs1 ^#s) \<subseteq> (trs2 ^#s)"
+shows "(trs1 ^#s) \<subseteq> (trs2 ^#s)"
using assms unfolding liftS_def[abs_def] by blast
-lemma lift_mono:
+lemma lift_mono:
assumes "\<phi> \<le> \<phi>'"
shows "(\<phi>^#) \<le> (\<phi>'^#)"
using assms unfolding lift_def[abs_def] by blast
@@ -249,20 +249,20 @@
shows "(\<phi>'^#2) as1 as2"
using assms unfolding lift2_def[abs_def] by blast
-lemma lift2_mono:
+lemma lift2_mono:
assumes "\<phi> \<le> \<phi>'"
shows "(\<phi>^#2) \<le> (\<phi>'^#2)"
-using assms unfolding lift2_def[abs_def] by blast
+using assms unfolding lift2_def[abs_def] by blast
lemma finite_cont[simp]: "finite (cont tr)"
unfolding cont_def by auto
-theorem Node_root_cont[simp]:
+theorem Node_root_cont[simp]:
"Node (root tr) (cont tr) = tr"
using NNode_root_ccont unfolding Node_def cont_def
by (metis cont_def finite_cont fset_cong fset_to_fset o_def)
-theorem Tree_simps[simp]:
+theorem Tree_simps[simp]:
assumes "finite as" and "finite as'"
shows "Node n as = Node n' as' \<longleftrightarrow> n = n' \<and> as = as'"
using assms TTree_simps unfolding Node_def
@@ -276,18 +276,18 @@
by (metis Node Node_root_cont finite_cont)
theorem Tree_sel_ctor[simp]:
-"root (Node n as) = n"
-"finite as \<Longrightarrow> cont (Node n as) = as"
+"root (Node n as) = n"
+"finite as \<Longrightarrow> cont (Node n as) = as"
unfolding Node_def cont_def by auto
theorems root_Node = Tree_sel_ctor(1)
theorems cont_Node = Tree_sel_ctor(2)
theorem Tree_coind_Node[elim, consumes 1, case_names Node]:
-assumes phi: "\<phi> tr1 tr2" and
-Node:
-"\<And> n1 n2 as1 as2.
- \<lbrakk>finite as1; finite as2; \<phi> (Node n1 as1) (Node n2 as2)\<rbrakk>
+assumes phi: "\<phi> tr1 tr2" and
+Node:
+"\<And> n1 n2 as1 as2.
+ \<lbrakk>finite as1; finite as2; \<phi> (Node n1 as1) (Node n2 as2)\<rbrakk>
\<Longrightarrow> n1 = n2 \<and> (\<phi>^#2) as1 as2"
shows "tr1 = tr2"
using phi apply(induct rule: TTree_coind_Node)
@@ -298,15 +298,15 @@
by (metis finite_fset fset_cong fset_to_fset)
theorem Tree_coind[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
-assumes phi: "\<phi> tr1 tr2" and
-Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
+assumes phi: "\<phi> tr1 tr2" and
+Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
root tr1 = root tr2 \<and> (\<phi>^#2) (cont tr1) (cont tr2)"
shows "tr1 = tr2"
using phi apply(induct rule: TTree_coind)
unfolding llift2_lift2 apply(rule Lift[unfolded cont_def comp_def]) .
-theorem coit:
-"root (coit rt ct b) = rt b"
+theorem coit:
+"root (coit rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (coit rt ct b) = image (id \<oplus> coit rt ct) (ct b)"
using TTree_coit[of rt "the_inv fset \<circ> ct" b] unfolding coit_def
apply - apply metis
@@ -314,8 +314,8 @@
by (metis (no_types) fset_to_fset map_fset_image)
-theorem corec:
-"root (corec rt ct b) = rt b"
+theorem corec:
+"root (corec rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
using TTree_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
apply - apply metis
--- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Tue Sep 04 17:23:08 2012 +0200
@@ -137,25 +137,25 @@
"\<And> xtas t a. sumJoin4 var app lam lt (Inr (Inr (Inr (xtas,(t,a))))) = lt xtas t a"
unfolding sumJoin4_def by auto
-definition "trmrec var app lam lt \<equiv> trm_rec (sumJoin4 var app lam lt)"
+definition "trmrec var app lam lt \<equiv> trm_fld_rec (sumJoin4 var app lam lt)"
lemma trmrec_Var[simp]:
"trmrec var app lam lt (Var x) = var x"
-unfolding trmrec_def Var_def trm.rec trmBNF_map(1) by simp
+unfolding trmrec_def Var_def trm.fld_rec trmBNF_map(1) by simp
lemma trmrec_App[simp]:
"trmrec var app lam lt (App t1 t2) =
app t1 (trmrec var app lam lt t1) t2 (trmrec var app lam lt t2)"
-unfolding trmrec_def App_def trm.rec trmBNF_map(2) convol_def by simp
+unfolding trmrec_def App_def trm.fld_rec trmBNF_map(2) convol_def by simp
lemma trmrec_Lam[simp]:
"trmrec var app lam lt (Lam x t) = lam x t (trmrec var app lam lt t)"
-unfolding trmrec_def Lam_def trm.rec trmBNF_map(3) convol_def by simp
+unfolding trmrec_def Lam_def trm.fld_rec trmBNF_map(3) convol_def by simp
lemma trmrec_Lt[simp]:
"trmrec var app lam lt (Lt xts t) =
lt (map_fset (\<lambda> (x,t). (x,t,trmrec var app lam lt t)) xts) t (trmrec var app lam lt t)"
-unfolding trmrec_def Lt_def trm.rec trmBNF_map(4) convol_def by simp
+unfolding trmrec_def Lt_def trm.fld_rec trmBNF_map(4) convol_def by simp
definition
"sumJoinI4 f1 f2 f3 f4 \<equiv>
@@ -174,25 +174,25 @@
unfolding sumJoinI4_def by auto
(* The iterator has a simpler, hence more manageable type. *)
-definition "trmiter var app lam lt \<equiv> trm_iter (sumJoinI4 var app lam lt)"
+definition "trmiter var app lam lt \<equiv> trm_fld_iter (sumJoinI4 var app lam lt)"
lemma trmiter_Var[simp]:
"trmiter var app lam lt (Var x) = var x"
-unfolding trmiter_def Var_def trm.iter trmBNF_map(1) by simp
+unfolding trmiter_def Var_def trm.fld_iter trmBNF_map(1) by simp
lemma trmiter_App[simp]:
"trmiter var app lam lt (App t1 t2) =
app (trmiter var app lam lt t1) (trmiter var app lam lt t2)"
-unfolding trmiter_def App_def trm.iter trmBNF_map(2) by simp
+unfolding trmiter_def App_def trm.fld_iter trmBNF_map(2) by simp
lemma trmiter_Lam[simp]:
"trmiter var app lam lt (Lam x t) = lam x (trmiter var app lam lt t)"
-unfolding trmiter_def Lam_def trm.iter trmBNF_map(3) by simp
+unfolding trmiter_def Lam_def trm.fld_iter trmBNF_map(3) by simp
lemma trmiter_Lt[simp]:
"trmiter var app lam lt (Lt xts t) =
lt (map_fset (\<lambda> (x,t). (x,trmiter var app lam lt t)) xts) (trmiter var app lam lt t)"
-unfolding trmiter_def Lt_def trm.iter trmBNF_map(4) by simp
+unfolding trmiter_def Lt_def trm.fld_iter trmBNF_map(4) by simp
subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *}
--- a/src/HOL/Codatatype/Examples/ListF.thy Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/ListF.thy Tue Sep 04 17:23:08 2012 +0200
@@ -18,27 +18,27 @@
definition "Conss a as \<equiv> listF_fld (Inr (a, as))"
lemma listF_map_NilF[simp]: "listF_map f NilF = NilF"
-unfolding listF_map_def listFBNF_map_def NilF_def listF.iter by simp
+unfolding listF_map_def listFBNF_map_def NilF_def listF.fld_iter by simp
lemma listF_map_Conss[simp]:
"listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)"
-unfolding listF_map_def listFBNF_map_def Conss_def listF.iter by simp
+unfolding listF_map_def listFBNF_map_def Conss_def listF.fld_iter by simp
lemma listF_set_NilF[simp]: "listF_set NilF = {}"
-unfolding listF_set_def NilF_def listF.iter listFBNF_set1_def listFBNF_set2_def
+unfolding listF_set_def NilF_def listF.fld_iter listFBNF_set1_def listFBNF_set2_def
sum_set_defs listFBNF_map_def collect_def[abs_def] by simp
lemma listF_set_Conss[simp]: "listF_set (Conss x xs) = {x} \<union> listF_set xs"
-unfolding listF_set_def Conss_def listF.iter listFBNF_set1_def listFBNF_set2_def
+unfolding listF_set_def Conss_def listF.fld_iter listFBNF_set1_def listFBNF_set2_def
sum_set_defs prod_set_defs listFBNF_map_def collect_def[abs_def] by simp
-lemma iter_sum_case_NilF: "listF_iter (sum_case f g) NilF = f ()"
-unfolding NilF_def listF.iter listFBNF_map_def by simp
+lemma iter_sum_case_NilF: "listF_fld_iter (sum_case f g) NilF = f ()"
+unfolding NilF_def listF.fld_iter listFBNF_map_def by simp
lemma iter_sum_case_Conss:
- "listF_iter (sum_case f g) (Conss y ys) = g (y, listF_iter (sum_case f g) ys)"
-unfolding Conss_def listF.iter listFBNF_map_def by simp
+ "listF_fld_iter (sum_case f g) (Conss y ys) = g (y, listF_fld_iter (sum_case f g) ys)"
+unfolding Conss_def listF.fld_iter listFBNF_map_def by simp
(* familiar induction principle *)
lemma listF_induct:
@@ -71,9 +71,9 @@
[simp]: "Singll a \<equiv> Conss a NilF"
definition appendd (infixr "@@" 65) where
- "appendd \<equiv> listF_iter (sum_case (\<lambda> _. id) (\<lambda> (a,f) bs. Conss a (f bs)))"
+ "appendd \<equiv> listF_fld_iter (sum_case (\<lambda> _. id) (\<lambda> (a,f) bs. Conss a (f bs)))"
-definition "lrev \<equiv> listF_iter (sum_case (\<lambda> _. NilF) (\<lambda> (b,bs). bs @@ [[b]]))"
+definition "lrev \<equiv> listF_fld_iter (sum_case (\<lambda> _. NilF) (\<lambda> (b,bs). bs @@ [[b]]))"
lemma lrev_NilF[simp]: "lrev NilF = NilF"
unfolding lrev_def by (simp add: iter_sum_case_NilF)
--- a/src/HOL/Codatatype/Examples/Process.thy Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy Tue Sep 04 17:23:08 2012 +0200
@@ -290,7 +290,7 @@
('b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b)
\<Rightarrow>
'b \<Rightarrow> 'a process"
-where "pcoiter isA pr co isC c1 c2 \<equiv> process_coiter (join22 isA pr co isC c1 c2)"
+where "pcoiter isA pr co isC c1 c2 \<equiv> process_unf_coiter (join22 isA pr co isC c1 c2)"
lemma unf_prefOf:
assumes "process_unf q = Inl (a,p)"
@@ -325,8 +325,8 @@
fix P
let ?f = "pcoiter isA pr co isC c1 c2" let ?s = "join22 isA pr co isC c1 c2"
assume isA: "isA P"
- have unf: "process_unf (process_coiter ?s P) = Inl (pr P, ?f (co P))"
- using process.coiter[of ?s P]
+ have unf: "process_unf (process_unf_coiter ?s P) = Inl (pr P, ?f (co P))"
+ using process.unf_coiter[of ?s P]
unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA]
processBNF_map id_apply pcoiter_def .
thus "?f P = Action (pr P) (?f (co P))"
@@ -335,8 +335,8 @@
fix P
let ?f = "pcoiter isA pr co isC c1 c2" let ?s = "join22 isA pr co isC c1 c2"
assume isA: "\<not> isA P" and isC: "isC P"
- have unf: "process_unf (process_coiter ?s P) = Inr (?f (c1 P), ?f (c2 P))"
- using process.coiter[of ?s P]
+ have unf: "process_unf (process_unf_coiter ?s P) = Inr (?f (c1 P), ?f (c2 P))"
+ using process.unf_coiter[of ?s P]
unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
processBNF_map id_apply pcoiter_def .
thus "?f P = Choice (?f (c1 P)) (?f (c2 P))"
@@ -351,7 +351,7 @@
\<Rightarrow>
'b \<Rightarrow> 'a process"
where
-"pcorec isA pr co isC c1 c2 \<equiv> process_corec (join22 isA pr co isC c1 c2)"
+"pcorec isA pr co isC c1 c2 \<equiv> process_unf_corec (join22 isA pr co isC c1 c2)"
theorem pcorec_Action:
assumes isA: "isA P"
@@ -366,15 +366,15 @@
show ?thesis
proof(cases "co P")
case (Inl p)
- have "process_unf (process_corec ?s P) = Inl (pr P, p)"
- using process.corec[of ?s P]
+ have "process_unf (process_unf_corec ?s P) = Inl (pr P, p)"
+ using process.unf_corec[of ?s P]
unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA]
processBNF_map id_apply pcorec_def Inl by simp
thus ?thesis unfolding Inl pcorec_def Action_def using process.fld_unf by (simp, metis)
next
case (Inr Q)
- have "process_unf (process_corec ?s P) = Inl (pr P, ?f Q)"
- using process.corec[of ?s P]
+ have "process_unf (process_unf_corec ?s P) = Inl (pr P, ?f Q)"
+ using process.unf_corec[of ?s P]
unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA]
processBNF_map id_apply pcorec_def Inr by simp
thus ?thesis unfolding Inr pcorec_def Action_def using process.fld_unf by (simp, metis)
@@ -404,15 +404,15 @@
show ?thesis
proof(cases "c2 P")
case (Inl p2) note c2 = Inl
- have "process_unf (process_corec ?s P) = Inr (p1, p2)"
- using process.corec[of ?s P]
+ have "process_unf (process_unf_corec ?s P) = Inr (p1, p2)"
+ using process.unf_corec[of ?s P]
unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
processBNF_map id_apply pcorec_def c1 c2 by simp
thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis)
next
case (Inr Q2) note c2 = Inr
- have "process_unf (process_corec ?s P) = Inr (p1, ?f Q2)"
- using process.corec[of ?s P]
+ have "process_unf (process_unf_corec ?s P) = Inr (p1, ?f Q2)"
+ using process.unf_corec[of ?s P]
unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
processBNF_map id_apply pcorec_def c1 c2 by simp
thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis)
@@ -422,15 +422,15 @@
show ?thesis
proof(cases "c2 P")
case (Inl p2) note c2 = Inl
- have "process_unf (process_corec ?s P) = Inr (?f Q1, p2)"
- using process.corec[of ?s P]
+ have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, p2)"
+ using process.unf_corec[of ?s P]
unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
processBNF_map id_apply pcorec_def c1 c2 by simp
thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis)
next
case (Inr Q2) note c2 = Inr
- have "process_unf (process_corec ?s P) = Inr (?f Q1, ?f Q2)"
- using process.corec[of ?s P]
+ have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, ?f Q2)"
+ using process.unf_corec[of ?s P]
unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
processBNF_map id_apply pcorec_def c1 c2 by simp
thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis)
--- a/src/HOL/Codatatype/Examples/Stream.thy Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Stream.thy Tue Sep 04 17:23:08 2012 +0200
@@ -18,12 +18,12 @@
definition "hdd as \<equiv> fst (stream_unf as)"
definition "tll as \<equiv> snd (stream_unf as)"
-lemma coiter_pair_fun_hdd[simp]: "hdd (stream_coiter (f \<odot> g) t) = f t"
-unfolding hdd_def pair_fun_def stream.coiter by simp
+lemma coiter_pair_fun_hdd[simp]: "hdd (stream_unf_coiter (f \<odot> g) t) = f t"
+unfolding hdd_def pair_fun_def stream.unf_coiter by simp
-lemma coiter_pair_fun_tll[simp]: "tll (stream_coiter (f \<odot> g) t) =
- stream_coiter (f \<odot> g) (g t)"
-unfolding tll_def pair_fun_def stream.coiter by simp
+lemma coiter_pair_fun_tll[simp]: "tll (stream_unf_coiter (f \<odot> g) t) =
+ stream_unf_coiter (f \<odot> g) (g t)"
+unfolding tll_def pair_fun_def stream.unf_coiter by simp
(* infinite trees: *)
coinductive infiniteTr where
@@ -45,7 +45,7 @@
"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
by (erule infiniteTr.cases) blast
-definition "konigPath \<equiv> stream_coiter
+definition "konigPath \<equiv> stream_unf_coiter
(lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t"
@@ -111,7 +111,7 @@
(* some more stream theorems *)
-lemma stream_map[simp]: "stream_map f = stream_coiter (f o hdd \<odot> tll)"
+lemma stream_map[simp]: "stream_map f = stream_unf_coiter (f o hdd \<odot> tll)"
unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def]
map_pair_def o_def prod_case_beta by simp
@@ -123,13 +123,13 @@
definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
[simp]: "plus xs ys =
- stream_coiter ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
+ stream_unf_coiter ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
[simp]: "scalar n = stream_map (\<lambda>x. n * x)"
-definition ones :: "nat stream" where [simp]: "ones = stream_coiter ((%x. 1) \<odot> id) ()"
-definition twos :: "nat stream" where [simp]: "twos = stream_coiter ((%x. 2) \<odot> id) ()"
+definition ones :: "nat stream" where [simp]: "ones = stream_unf_coiter ((%x. 1) \<odot> id) ()"
+definition twos :: "nat stream" where [simp]: "twos = stream_unf_coiter ((%x. 2) \<odot> id) ()"
definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
lemma "ones \<oplus> ones = twos"
--- a/src/HOL/Codatatype/Examples/TreeFI.thy Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFI.thy Tue Sep 04 17:23:08 2012 +0200
@@ -30,14 +30,14 @@
definition pair_fun (infixr "\<odot>" 50) where
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
-lemma coiter_pair_fun_lab: "lab (treeFI_coiter (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFI.coiter treeFIBNF_map_def by simp
+lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \<odot> g) t) = f t"
+unfolding lab_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp
-lemma coiter_pair_fun_sub: "sub (treeFI_coiter (f \<odot> g) t) = listF_map (treeFI_coiter (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFI.coiter treeFIBNF_map_def by simp
+lemma coiter_pair_fun_sub: "sub (treeFI_unf_coiter (f \<odot> g) t) = listF_map (treeFI_unf_coiter (f \<odot> g)) (g t)"
+unfolding sub_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp
(* Tree reverse:*)
-definition "trev \<equiv> treeFI_coiter (lab \<odot> lrev o sub)"
+definition "trev \<equiv> treeFI_unf_coiter (lab \<odot> lrev o sub)"
lemma trev_simps1[simp]: "lab (trev t) = lab t"
unfolding trev_def by (simp add: coiter_pair_fun_lab)
--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Tue Sep 04 17:23:08 2012 +0200
@@ -26,14 +26,14 @@
lemma unf[simp]: "treeFsetI_unf t = (lab t, sub t)"
unfolding lab_def sub_def by simp
-lemma coiter_pair_fun_lab: "lab (treeFsetI_coiter (f \<odot> g) t) = f t"
-unfolding lab_def pair_fun_def treeFsetI.coiter treeFsetIBNF_map_def by simp
+lemma coiter_pair_fun_lab: "lab (treeFsetI_unf_coiter (f \<odot> g) t) = f t"
+unfolding lab_def pair_fun_def treeFsetI.unf_coiter treeFsetIBNF_map_def by simp
-lemma coiter_pair_fun_sub: "sub (treeFsetI_coiter (f \<odot> g) t) = map_fset (treeFsetI_coiter (f \<odot> g)) (g t)"
-unfolding sub_def pair_fun_def treeFsetI.coiter treeFsetIBNF_map_def by simp
+lemma coiter_pair_fun_sub: "sub (treeFsetI_unf_coiter (f \<odot> g) t) = map_fset (treeFsetI_unf_coiter (f \<odot> g)) (g t)"
+unfolding sub_def pair_fun_def treeFsetI.unf_coiter treeFsetIBNF_map_def by simp
(* tree map (contrived example): *)
-definition "tmap f \<equiv> treeFsetI_coiter (f o lab \<odot> sub)"
+definition "tmap f \<equiv> treeFsetI_unf_coiter (f o lab \<odot> sub)"
lemma tmap_simps1[simp]: "lab (tmap f t) = f (lab t)"
unfolding tmap_def by (simp add: coiter_pair_fun_lab)
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 04 17:23:08 2012 +0200
@@ -18,15 +18,17 @@
val coN: string
val coinductN: string
val coiterN: string
- val coiter_uniqueN: string
+ val unf_coiter_uniqueN: string
val corecN: string
val exhaustN: string
val fldN: string
- val fld_coiterN: string
+ val fld_unf_coiterN: string
val fld_exhaustN: string
val fld_induct2N: string
val fld_inductN: string
val fld_injectN: string
+ val fld_iterN: string
+ val fld_recN: string
val fld_unfN: string
val hsetN: string
val hset_recN: string
@@ -34,7 +36,7 @@
val injectN: string
val isNodeN: string
val iterN: string
- val iter_uniqueN: string
+ val fld_iter_uniqueN: string
val lsbisN: string
val map_simpsN: string
val map_uniqueN: string
@@ -56,6 +58,8 @@
val unfN: string
val unf_coinductN: string
val unf_coinduct_uptoN: string
+ val unf_coiterN: string
+ val unf_corecN: string
val unf_exhaustN: string
val unf_fldN: string
val unf_injectN: string
@@ -127,11 +131,13 @@
val iterN = "iter"
val coiterN = coN ^ iterN
val uniqueN = "_unique"
-val iter_uniqueN = iterN ^ uniqueN
-val coiter_uniqueN = coiterN ^ uniqueN
val fldN = "fld"
val unfN = "unf"
-val fld_coiterN = fldN ^ "_" ^ coiterN
+val fld_iterN = fldN ^ "_" ^ iterN
+val unf_coiterN = unfN ^ "_" ^ coiterN
+val fld_iter_uniqueN = fld_iterN ^ uniqueN
+val unf_coiter_uniqueN = unf_coiterN ^ uniqueN
+val fld_unf_coiterN = fldN ^ "_" ^ unf_coiterN
val map_simpsN = mapN ^ "_simps"
val map_uniqueN = mapN ^ uniqueN
val min_algN = "min_alg"
@@ -153,6 +159,8 @@
val str_initN = "str_init"
val recN = "rec"
val corecN = coN ^ recN
+val fld_recN = fldN ^ "_" ^ recN
+val unf_corecN = unfN ^ "_" ^ corecN
val fld_unfN = fldN ^ "_" ^ unfN
val unf_fldN = unfN ^ "_" ^ fldN
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 17:23:08 2012 +0200
@@ -1938,7 +1938,7 @@
val timer = time (timer "unf definitions & thms");
- fun coiter_bind i = Binding.suffix_name ("_" ^ coN ^ iterN) (nth bs (i - 1));
+ fun coiter_bind i = Binding.suffix_name ("_" ^ unf_coiterN) (nth bs (i - 1));
val coiter_name = Binding.name_of o coiter_bind;
val coiter_def_bind = rpair [] o Thm.def_binding o coiter_bind;
@@ -2129,7 +2129,7 @@
trans OF [mor RS unique, coiter_unf]) coiter_unique_mor_thms coiter_unf_thms
end;
- fun corec_bind i = Binding.suffix_name ("_" ^ coN ^ recN) (nth bs (i - 1));
+ fun corec_bind i = Binding.suffix_name ("_" ^ unf_corecN) (nth bs (i - 1));
val corec_name = Binding.name_of o corec_bind;
val corec_def_bind = rpair [] o Thm.def_binding o corec_bind;
@@ -2973,16 +2973,16 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val notes =
- [(coiterN, coiter_thms),
- (coiter_uniqueN, coiter_unique_thms),
- (corecN, corec_thms),
+ [(unf_coiterN, coiter_thms),
+ (unf_coiter_uniqueN, coiter_unique_thms),
+ (unf_corecN, corec_thms),
(unf_fldN, unf_fld_thms),
(fld_unfN, fld_unf_thms),
(unf_injectN, unf_inject_thms),
(unf_exhaustN, unf_exhaust_thms),
(fld_injectN, fld_inject_thms),
(fld_exhaustN, fld_exhaust_thms),
- (fld_coiterN, fld_coiter_thms)]
+ (fld_unf_coiterN, fld_coiter_thms)]
|> map (apsnd (map single))
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 16:27:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 17:23:08 2012 +0200
@@ -1052,7 +1052,7 @@
(mk_mor UNIVs flds active_UNIVs ss (map (mk_nthN n iter_f) ks));
val iter = HOLogic.choice_const iterT $ iter_fun;
- fun iter_bind i = Binding.suffix_name ("_" ^ iterN) (nth bs (i - 1));
+ fun iter_bind i = Binding.suffix_name ("_" ^ fld_iterN) (nth bs (i - 1));
val iter_name = Binding.name_of o iter_bind;
val iter_def_bind = rpair [] o Thm.def_binding o iter_bind;
@@ -1210,7 +1210,7 @@
trans OF [mor RS unique, iter_fld]) iter_unique_mor_thms iter_fld_thms
end;
- fun rec_bind i = Binding.suffix_name ("_" ^ recN) (nth bs (i - 1));
+ fun rec_bind i = Binding.suffix_name ("_" ^ fld_recN) (nth bs (i - 1));
val rec_name = Binding.name_of o rec_bind;
val rec_def_bind = rpair [] o Thm.def_binding o rec_bind;
@@ -1797,9 +1797,9 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val notes =
- [(iterN, iter_thms),
- (iter_uniqueN, iter_unique_thms),
- (recN, rec_thms),
+ [(fld_iterN, iter_thms),
+ (fld_iter_uniqueN, iter_unique_thms),
+ (fld_recN, rec_thms),
(unf_fldN, unf_fld_thms),
(fld_unfN, fld_unf_thms),
(unf_injectN, unf_inject_thms),