--- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Sat Sep 08 21:04:27 2012 +0200
@@ -24,14 +24,14 @@
(* 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
+lemma pre_Tree_map:
+"pre_Tree_map f (n, as) = (n, map_fset (id \<oplus> f) as)"
+unfolding pre_Tree_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)
+lemma pre_Tree_map':
+"pre_Tree_map f n_as = (fst n_as, map_fset (id \<oplus> f) (snd n_as))"
+using pre_Tree_map by(cases n_as, simp)
definition
@@ -40,8 +40,8 @@
(\<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"
-unfolding llift2_def TreeBNF.pred_unfold
+lemma pre_Tree_pred: "pre_Tree_pred \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> as1 as2"
+unfolding llift2_def pre_Tree.pred_unfold
apply (auto split: sum.splits)
apply (metis sumE)
apply (metis sumE)
@@ -132,11 +132,11 @@
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 "pre_Tree_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(case_tac x, case_tac xa, simp)
- unfolding TreeBNF_pred apply(rule NNode) using \<phi> unfolding NNode_def by simp
+ unfolding pre_Tree_pred apply(rule NNode) using \<phi> unfolding NNode_def by simp
qed
theorem TTree_coind[elim, consumes 1, case_names LLift]:
@@ -178,7 +178,7 @@
"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.unf_coiter[of "<rt,ct>" b] unfolding Tree_coit_coit fst_convol snd_convol
-unfolding TreeBNF_map' fst_convol' snd_convol'
+unfolding pre_Tree_map' fst_convol' snd_convol'
unfolding Tree_unf_root_ccont by simp_all
(* Corecursion, stronger than coiteration *)
@@ -195,7 +195,7 @@
"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.unf_corec[of "<rt,ct>" b] unfolding Tree_unf_corec_corec fst_convol snd_convol
-unfolding TreeBNF_map' fst_convol' snd_convol'
+unfolding pre_Tree_map' fst_convol' snd_convol'
unfolding Tree_unf_root_ccont by simp_all
--- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Sat Sep 08 21:04:27 2012 +0200
@@ -22,26 +22,26 @@
subsection{* Set and map *}
-lemma trmBNF_set2_Lt: "trmBNF_set2 (Inr (Inr (Inr (xts, t)))) = snd ` (fset xts) \<union> {t}"
-unfolding trmBNF_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
+lemma pre_trm_set2_Lt: "pre_trm_set2 (Inr (Inr (Inr (xts, t)))) = snd ` (fset xts) \<union> {t}"
+unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
by auto
-lemma trmBNF_set2_Var: "\<And>x. trmBNF_set2 (Inl x) = {}"
-and trmBNF_set2_App:
-"\<And>t1 t2. trmBNF_set2 (Inr (Inl t1t2)) = {fst t1t2, snd t1t2}"
-and trmBNF_set2_Lam:
-"\<And>x t. trmBNF_set2 (Inr (Inr (Inl (x, t)))) = {t}"
-unfolding trmBNF_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
+lemma pre_trm_set2_Var: "\<And>x. pre_trm_set2 (Inl x) = {}"
+and pre_trm_set2_App:
+"\<And>t1 t2. pre_trm_set2 (Inr (Inl t1t2)) = {fst t1t2, snd t1t2}"
+and pre_trm_set2_Lam:
+"\<And>x t. pre_trm_set2 (Inr (Inr (Inl (x, t)))) = {t}"
+unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
by auto
-lemma trmBNF_map:
-"\<And> a1. trmBNF_map f1 f2 (Inl a1) = Inl (f1 a1)"
-"\<And> a2 b2. trmBNF_map f1 f2 (Inr (Inl (a2,b2))) = Inr (Inl (f2 a2, f2 b2))"
-"\<And> a1 a2. trmBNF_map f1 f2 (Inr (Inr (Inl (a1,a2)))) = Inr (Inr (Inl (f1 a1, f2 a2)))"
+lemma pre_trm_map:
+"\<And> a1. pre_trm_map f1 f2 (Inl a1) = Inl (f1 a1)"
+"\<And> a2 b2. pre_trm_map f1 f2 (Inr (Inl (a2,b2))) = Inr (Inl (f2 a2, f2 b2))"
+"\<And> a1 a2. pre_trm_map f1 f2 (Inr (Inr (Inl (a1,a2)))) = Inr (Inr (Inl (f1 a1, f2 a2)))"
"\<And> a1a2s a2.
- trmBNF_map f1 f2 (Inr (Inr (Inr (a1a2s, a2)))) =
+ pre_trm_map f1 f2 (Inr (Inr (Inr (a1a2s, a2)))) =
Inr (Inr (Inr (map_fset (\<lambda> (a1', a2'). (f1 a1', f2 a2')) a1a2s, f2 a2)))"
-unfolding trmBNF_map_def collect_def[abs_def] map_pair_def by auto
+unfolding pre_trm_map_def collect_def[abs_def] map_pair_def by auto
subsection{* Constructors *}
@@ -87,7 +87,7 @@
shows "phi t"
proof(induct rule: trm.fld_induct)
fix u :: "'a + 'a trm \<times> 'a trm + 'a \<times> 'a trm + ('a \<times> 'a trm) fset \<times> 'a trm"
- assume IH: "\<And>t. t \<in> trmBNF_set2 u \<Longrightarrow> phi t"
+ assume IH: "\<And>t. t \<in> pre_trm_set2 u \<Longrightarrow> phi t"
show "phi (trm_fld u)"
proof(cases u)
case (Inl x)
@@ -99,7 +99,7 @@
case (Inl t1t2)
obtain t1 t2 where t1t2: "t1t2 = (t1,t2)" by (cases t1t2, blast)
show ?thesis unfolding Inr1 Inl t1t2 App_def[symmetric] apply(rule App)
- using IH unfolding Inr1 Inl trmBNF_set2_App t1t2 fst_conv snd_conv by blast+
+ using IH unfolding Inr1 Inl pre_trm_set2_App t1t2 fst_conv snd_conv by blast+
next
case (Inr uuu) note Inr2 = Inr
show ?thesis
@@ -107,12 +107,12 @@
case (Inl xt)
obtain x t where xt: "xt = (x,t)" by (cases xt, blast)
show ?thesis unfolding Inr1 Inr2 Inl xt Lam_def[symmetric] apply(rule Lam)
- using IH unfolding Inr1 Inr2 Inl trmBNF_set2_Lam xt by blast
+ using IH unfolding Inr1 Inr2 Inl pre_trm_set2_Lam xt by blast
next
case (Inr xts_t)
obtain xts t where xts_t: "xts_t = (xts,t)" by (cases xts_t, blast)
show ?thesis unfolding Inr1 Inr2 Inr xts_t Lt_def[symmetric] apply(rule Lt) using IH
- unfolding Inr1 Inr2 Inr trmBNF_set2_Lt xts_t fset_fset_member image_def by auto
+ unfolding Inr1 Inr2 Inr pre_trm_set2_Lt xts_t fset_fset_member image_def by auto
qed
qed
qed
@@ -141,21 +141,21 @@
lemma trmrec_Var[simp]:
"trmrec var app lam lt (Var x) = var x"
-unfolding trmrec_def Var_def trm.fld_rec trmBNF_map(1) by simp
+unfolding trmrec_def Var_def trm.fld_rec pre_trm_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.fld_rec trmBNF_map(2) convol_def by simp
+unfolding trmrec_def App_def trm.fld_rec pre_trm_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.fld_rec trmBNF_map(3) convol_def by simp
+unfolding trmrec_def Lam_def trm.fld_rec pre_trm_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.fld_rec trmBNF_map(4) convol_def by simp
+unfolding trmrec_def Lt_def trm.fld_rec pre_trm_map(4) convol_def by simp
definition
"sumJoinI4 f1 f2 f3 f4 \<equiv>
@@ -178,21 +178,21 @@
lemma trmiter_Var[simp]:
"trmiter var app lam lt (Var x) = var x"
-unfolding trmiter_def Var_def trm.fld_iter trmBNF_map(1) by simp
+unfolding trmiter_def Var_def trm.fld_iter pre_trm_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.fld_iter trmBNF_map(2) by simp
+unfolding trmiter_def App_def trm.fld_iter pre_trm_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.fld_iter trmBNF_map(3) by simp
+unfolding trmiter_def Lam_def trm.fld_iter pre_trm_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.fld_iter trmBNF_map(4) by simp
+unfolding trmiter_def Lt_def trm.fld_iter pre_trm_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 Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Examples/ListF.thy Sat Sep 08 21:04:27 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.fld_iter by simp
+unfolding listF_map_def pre_listF_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.fld_iter by simp
+unfolding listF_map_def pre_listF_map_def Conss_def listF.fld_iter by simp
lemma listF_set_NilF[simp]: "listF_set NilF = {}"
-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
+unfolding listF_set_def NilF_def listF.fld_iter pre_listF_set1_def pre_listF_set2_def
+ sum_set_defs pre_listF_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.fld_iter listFBNF_set1_def listFBNF_set2_def
- sum_set_defs prod_set_defs listFBNF_map_def collect_def[abs_def] by simp
+unfolding listF_set_def Conss_def listF.fld_iter pre_listF_set1_def pre_listF_set2_def
+ sum_set_defs prod_set_defs pre_listF_map_def collect_def[abs_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
+unfolding NilF_def listF.fld_iter pre_listF_map_def by simp
lemma iter_sum_case_Conss:
"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
+unfolding Conss_def listF.fld_iter pre_listF_map_def by simp
(* familiar induction principle *)
lemma listF_induct:
@@ -47,7 +47,7 @@
shows "P xs"
proof (rule listF.fld_induct)
fix xs :: "unit + 'a \<times> 'a listF"
- assume raw_IH: "\<And>a. a \<in> listFBNF_set2 xs \<Longrightarrow> P a"
+ assume raw_IH: "\<And>a. a \<in> pre_listF_set2 xs \<Longrightarrow> P a"
show "P (listF_fld xs)"
proof (cases xs)
case (Inl a) with IB show ?thesis unfolding NilF_def by simp
@@ -55,8 +55,8 @@
case (Inr b)
then obtain y ys where yys: "listF_fld xs = Conss y ys"
unfolding Conss_def listF.fld_inject by (blast intro: prod.exhaust)
- hence "ys \<in> listFBNF_set2 xs"
- unfolding listFBNF_set2_def Conss_def listF.fld_inject sum_set_defs prod_set_defs
+ hence "ys \<in> pre_listF_set2 xs"
+ unfolding pre_listF_set2_def Conss_def listF.fld_inject sum_set_defs prod_set_defs
collect_def[abs_def] by simp
with raw_IH have "P ys" by blast
with IH have "P (Conss y ys)" by blast
--- a/src/HOL/Codatatype/Examples/Process.thy Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy Sat Sep 08 21:04:27 2012 +0200
@@ -25,17 +25,17 @@
(* These should be eventually inferred from compositionality *)
-lemma processBNF_map[simp]:
-"processBNF_map fa fp (Inl (a ,p)) = Inl (fa a, fp p)"
-"processBNF_map fa fp (Inr (p1, p2)) = Inr (fp p1, fp p2)"
-unfolding processBNF_map_def by auto
+lemma pre_process_map[simp]:
+"pre_process_map fa fp (Inl (a ,p)) = Inl (fa a, fp p)"
+"pre_process_map fa fp (Inr (p1, p2)) = Inr (fp p1, fp p2)"
+unfolding pre_process_map_def by auto
-lemma processBNF_pred[simp]:
-"processBNF_pred (op =) \<phi> (Inl (a,p)) (Inl (a',p')) \<longleftrightarrow> a = a' \<and> \<phi> p p'"
-"processBNF_pred (op =) \<phi> (Inr (p,q)) (Inr (p',q')) \<longleftrightarrow> \<phi> p p' \<and> \<phi> q q'"
-"\<not> processBNF_pred (op =) \<phi> (Inl ap) (Inr q1q2)"
-"\<not> processBNF_pred (op =) \<phi> (Inr q1q2) (Inl ap)"
-by (auto simp: diag_def processBNF.pred_unfold)
+lemma pre_process_pred[simp]:
+"pre_process_pred (op =) \<phi> (Inl (a,p)) (Inl (a',p')) \<longleftrightarrow> a = a' \<and> \<phi> p p'"
+"pre_process_pred (op =) \<phi> (Inr (p,q)) (Inr (p',q')) \<longleftrightarrow> \<phi> p p' \<and> \<phi> q q'"
+"\<not> pre_process_pred (op =) \<phi> (Inl ap) (Inr q1q2)"
+"\<not> pre_process_pred (op =) \<phi> (Inr q1q2) (Inl ap)"
+by (auto simp: diag_def pre_process.pred_unfold)
subsection{* Constructors *}
@@ -186,7 +186,7 @@
shows "p = p'"
proof(intro mp[OF process.pred_coinduct, of \<phi>, OF _ phi], clarify)
fix p p' assume \<phi>: "\<phi> p p'"
- show "processBNF_pred (op =) \<phi> (process_unf p) (process_unf p')"
+ show "pre_process_pred (op =) \<phi> (process_unf p) (process_unf p')"
proof(cases rule: process_cases[of p])
case (Action a q) note p = Action
hence "isAction p'" using iss[OF \<phi>] by (cases rule: process_cases[of p'], auto)
@@ -216,7 +216,7 @@
shows "p = p'"
proof(intro mp[OF process.pred_coinduct_upto, of \<phi>, OF _ phi], clarify)
fix p p' assume \<phi>: "\<phi> p p'"
- show "processBNF_pred (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_unf p) (process_unf p')"
+ show "pre_process_pred (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_unf p) (process_unf p')"
proof(cases rule: process_cases[of p])
case (Action a q) note p = Action
hence "isAction p'" using iss[OF \<phi>] by (cases rule: process_cases[of p'], auto)
@@ -328,7 +328,7 @@
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 .
+ pre_process_map id_apply pcoiter_def .
thus "?f P = Action (pr P) (?f (co P))"
unfolding pcoiter_def Action_def using process.fld_unf by metis
next
@@ -338,7 +338,7 @@
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 .
+ pre_process_map id_apply pcoiter_def .
thus "?f P = Choice (?f (c1 P)) (?f (c2 P))"
unfolding pcoiter_def Choice_def using process.fld_unf by metis
qed
@@ -369,14 +369,14 @@
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
+ pre_process_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_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
+ pre_process_map id_apply pcorec_def Inr by simp
thus ?thesis unfolding Inr pcorec_def Action_def using process.fld_unf by (simp, metis)
qed
qed
@@ -407,14 +407,14 @@
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
+ pre_process_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_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
+ pre_process_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)
qed
next
@@ -425,14 +425,14 @@
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
+ pre_process_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_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
+ pre_process_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)
qed
qed
--- a/src/HOL/Codatatype/Examples/Stream.thy Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Stream.thy Sat Sep 08 21:04:27 2012 +0200
@@ -115,10 +115,10 @@
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
-lemma streamBNF_pred[simp]: "streamBNF_pred \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))"
-by (auto simp: streamBNF.pred_unfold)
+lemma pre_stream_pred[simp]: "pre_stream_pred \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))"
+by (auto simp: pre_stream.pred_unfold)
-lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded streamBNF_pred[abs_def],
+lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded pre_stream_pred[abs_def],
folded hdd_def tll_def]
definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
--- a/src/HOL/Codatatype/Examples/TreeFI.thy Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFI.thy Sat Sep 08 21:04:27 2012 +0200
@@ -16,8 +16,8 @@
codata_raw treeFI: 'tree = "'a \<times> 'tree listF"
-lemma treeFIBNF_listF_set[simp]: "treeFIBNF_set2 (i, xs) = listF_set xs"
-unfolding treeFIBNF_set2_def collect_def[abs_def] prod_set_defs
+lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
+unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs
by (auto simp add: listF.set_natural')
(* selectors for trees *)
@@ -31,10 +31,10 @@
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
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
+unfolding lab_def pair_fun_def treeFI.unf_coiter pre_treeFI_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
+unfolding sub_def pair_fun_def treeFI.unf_coiter pre_treeFI_map_def by simp
(* Tree reverse:*)
definition "trev \<equiv> treeFI_unf_coiter (lab \<odot> lrev o sub)"
@@ -59,12 +59,12 @@
assume "phi a b"
with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)"
"\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i)" by auto
- hence "treeFIBNF_map id fst ?z = treeFI_unf a" "treeFIBNF_map id snd ?z = treeFI_unf b"
- unfolding treeFIBNF_map_def by auto
- moreover have "\<forall>(x, y) \<in> treeFIBNF_set2 ?z. phi x y"
+ hence "pre_treeFI_map id fst ?z = treeFI_unf a" "pre_treeFI_map id snd ?z = treeFI_unf b"
+ unfolding pre_treeFI_map_def by auto
+ moreover have "\<forall>(x, y) \<in> pre_treeFI_set2 ?z. phi x y"
proof safe
fix z1 z2
- assume "(z1, z2) \<in> treeFIBNF_set2 ?z"
+ assume "(z1, z2) \<in> pre_treeFI_set2 ?z"
hence "(z1, z2) \<in> listF_set ?zs" by auto
hence "\<exists>i < lengthh ?zs. nthh ?zs i = (z1, z2)" by auto
with step'(2) obtain i where "i < lengthh (sub a)"
@@ -72,9 +72,9 @@
with step'(3) show "phi z1 z2" by auto
qed
ultimately show "\<exists>z.
- (treeFIBNF_map id fst z = treeFI_unf a \<and>
- treeFIBNF_map id snd z = treeFI_unf b) \<and>
- (\<forall>x y. (x, y) \<in> treeFIBNF_set2 z \<longrightarrow> phi x y)" by blast
+ (pre_treeFI_map id fst z = treeFI_unf a \<and>
+ pre_treeFI_map id snd z = treeFI_unf b) \<and>
+ (\<forall>x y. (x, y) \<in> pre_treeFI_set2 z \<longrightarrow> phi x y)" by blast
qed
lemma trev_trev: "trev (trev tr) = tr"
--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Sat Sep 08 21:04:27 2012 +0200
@@ -27,10 +27,10 @@
unfolding lab_def sub_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
+unfolding lab_def pair_fun_def treeFsetI.unf_coiter pre_treeFsetI_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
+unfolding sub_def pair_fun_def treeFsetI.unf_coiter pre_treeFsetI_map_def by simp
(* tree map (contrived example): *)
definition "tmap f \<equiv> treeFsetI_unf_coiter (f o lab \<odot> sub)"
@@ -41,12 +41,12 @@
lemma trev_simps2[simp]: "sub (tmap f t) = map_fset (tmap f) (sub t)"
unfolding tmap_def by (simp add: coiter_pair_fun_sub)
-lemma treeFsetIBNF_pred[simp]: "treeFsetIBNF_pred R1 R2 a b = (R1 (fst a) (fst b) \<and>
+lemma pre_treeFsetI_pred[simp]: "pre_treeFsetI_pred R1 R2 a b = (R1 (fst a) (fst b) \<and>
(\<forall>t \<in> fset (snd a). (\<exists>u \<in> fset (snd b). R2 t u)) \<and>
(\<forall>t \<in> fset (snd b). (\<exists>u \<in> fset (snd a). R2 u t)))"
apply (cases a)
apply (cases b)
-apply (simp add: treeFsetIBNF.pred_unfold)
+apply (simp add: pre_treeFsetI.pred_unfold)
done
lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct]
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:04:27 2012 +0200
@@ -173,9 +173,11 @@
fun mk_iter_like Ts Us t =
let
val (binders, body) = strip_type (fastype_of t);
+val _ = tracing ("mk_iter_like: " ^ PolyML.makestring (binders, body, t)) (*###*)
val (f_Us, prebody) = split_last binders;
val Type (_, Ts0) = if lfp then prebody else body;
val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
+val _ = tracing (" Ts0 @ Us0 ...: " ^ PolyML.makestring (Ts0, Us0, Ts, Us)) (*###*)
in
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
@@ -371,6 +373,7 @@
val [iter_def, rec_def] = map (Morphism.thm phi) defs;
+val _ = tracing ("LFP As Cs: " ^ PolyML.makestring (As, Cs)) (*###*)
val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
in
((ctrs, iter, recx, v, xss, ctr_defs, iter_def, rec_def), lthy)
@@ -414,6 +417,7 @@
val [coiter_def, corec_def] = map (Morphism.thm phi) defs;
+val _ = tracing ("GFP As Cs: " ^ PolyML.makestring (As, Cs)) (*###*)
val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
in
((ctrs, coiter, corec, v, xss, ctr_defs, coiter_def, corec_def), lthy)